QED - an interactive textbook

Sections and exercises


This is version 2.10.7.

If the text has updated to a new version since your last session, you may need to reset the text in order for it to work correctly, or at least redo some of the exercises that unlock certain laws. This page works best when viewed on a large screen and with the ability to drag-and-drop; in particular, this page is unlikely to be all that functional on a cell phone. Also one may need a recently updated browser in order for the page to work properly (in particular, grid layouts and local storage should be supported for the best experience).

Further discussion of this text may be found at this blog post.

Here are some other interactive logic demonstrations:
IMPLICATION INTRODUCTION
AND
OR
IMPLIES
IFF
NOT
PUSH
PUSH (alternate form)
BICONDITIONAL INTRODUCTION
BICONDITIONAL ELIMINATION (left)
BICONDITIONAL ELIMINATION (right)
TRUE
NOT FALSE
NOT FALSE (alternate form)
PUSH (for free variables)
FREE VARIABLE INTRODUCTION
FOR ALL
THERE EXISTS
PUSH (for set variables)
PULL
PULL
EXISTENCE
EXISTENCE
EQUALITY IS REFLEXIVE
RENAMING BOUND VARIABLE (universal)
RENAMING BOUND VARIABLE (existential)
BARBARA SYLLOGISM (singular form)
  • The Root environment window below contains all the statements that one already knows to be true for the given exercise (which, in this case, are A, B and C). Initially this window will just contain the given hypotheses of the exercise.
  • Statements can be atomic formulas such as A, B, and C, or compound formulas formed from the atomic formulas and logical connectives such as AND, OR, and NOT. For instance, (A AND B) OR C is a compound formula, and thus a potential statement in one's argument.
  • If one drags one statement to another, the Available deductions window below will show what conclusions one can draw from these statements using the available deduction rules; if any conclusions can be drawn, one can add them to the Root environment window by clicking on the button containing the conclusion.
  • For instance, to solve this level one drags the A statement onto the B statement (or vice versa), clicks on the button marked "A AND B" to add that statement to the Root environment, drags the new A AND B statement onto the C statement (or vice versa), and then clicks on the button containing the desired conclusion.
  • By opening the first exercise of Section 1 (Exercise 1.1), you unlocked the rule of conjunction introduction. This asserts that if a statement A is known, and the statement B is known, then one can deduce the compound statement A AND B. This is the only rule one starts with, but more deductive rules will be unlocked whenever one begins a new section of the textbook. The Achievements window will record all the unlocked laws.
  • Progress is recorded in the Achievements and Event log windows below. This progress will be saved between sessions (assuming your browser supports local storage), unless you reset this interactive text completely using the button at the bottom of the page.
  • Your deductions will be recorded as a human-readable proof in the Proof window below. This window is not absolutely necessary in order to play the game, but should help you understand and interpret the moves you are making.
  • The exercise is completed when you have managed to obtain the desired conclusion (in this case, (A AND B) AND C) in the Root environment window. This will unlock further exercises and sections of the textbook, turning the exercise buttons from gray to yellow.
  1. A. [given]
  2. B. [given]
  3. C. [given]
  4. From A, B: deduce A AND B. [CONJUNCTION INTRODUCTION]
  5. From A AND B, C: deduce (A AND B) AND C. [CONJUNCTION INTRODUCTION]
  6. QED!
AND IS IDEMPOTENT
  • It is permissible to drag a statement onto itself.
  • You can move forwards and backwards through the unlocked exercises using the "PREVIOUS EXERCISE" and "NEXT EXERCISE" buttons at the bottom of this page, or by using the '<' and '>' hotkeys.
  1. A. [given]
  2. From A, A: deduce A AND A. [CONJUNCTION INTRODUCTION]
  3. QED!
AND IS COMMUTATIVE
  • The rules of conjunction elimination have been unlocked. These rules assert that if a conjunction statement such as A AND B is known, then one can deduce either of the two individual statements A or B of that statement separately.
  • To activate this rule, click on a compound statement of the form A AND B.
  1. A AND B. [given]
  2. From A AND B: deduce A. [CONJUNCTION ELIMINATION (left)]
  3. From A AND B: deduce B. [CONJUNCTION ELIMINATION (right)]
  4. From B, A: deduce B AND A. [CONJUNCTION INTRODUCTION]
  5. QED!
AND IS ASSOCIATIVE (left)
  • One can think of a deduction rule as a template in which the atomic formulas of the deduction rule (such as A or B) can be replaced by compound formulas (e.g. "A AND B"). This can greatly increase the power of such laws.
  • Each problem that I solved became a rule, which served afterwards to solve other problems - René Descartes. Each exercise solved in this text becomes a new deduction rule that you may use in subsequent exercises. The Achievements window lists all the rules of inference one has available, either through being unlocked by opening the appropriate exercise, or by proving that rule as one of the exercises.
  • One can also use the numbers '1' through '9' as hotkeys for the available eductions (or the first 9 of them, at any rate).
  1. (A AND B) AND C. [given]
  2. From (A AND B) AND C: deduce A AND B. [CONJUNCTION ELIMINATION (left)]
  3. From (A AND B) AND C: deduce C. [CONJUNCTION ELIMINATION (right)]
  4. From A AND B: deduce A. [CONJUNCTION ELIMINATION (left)]
  5. From A AND B: deduce B. [CONJUNCTION ELIMINATION (right)]
  6. From B, C: deduce B AND C. [CONJUNCTION INTRODUCTION]
  7. From A, B AND C: deduce A AND (B AND C). [CONJUNCTION INTRODUCTION]
  8. QED!
AND IS ASSOCIATIVE (right)
  • There are no "wrong" moves in the QED game - every move you make is a valid deduction! However, you may end up making "useless" moves - moves that are logically valid, but do not bring one closer to the desired conclusion. If you are finding the deduction environment to be getting too cluttered, you can click on the exercise button (in this case, Exercise 2.2(b)) to start from the beginning; one can also press the "RESTART EXERCISE" (or presses "r") at the bottom of the page.
  • One can also delete sentences by selecting them and then pressing the delete key, though one should caution that this may render the exercise unsolvable without a restart if a key hypothesis ends up being deleted.
  • Finally, one can also "UNDO" a deduction if one presses the "IMMEDIATE UNDO" button at the bottom of this page (or presses "u") immediately after making a deduction. This feature is not available if the deduction solves the exercise, or if one has performed any action between the deduction and the undo.
  • Thanks to Stijn Vanhee and Siddhartha Srivastava for supplying a short proof.
  1. A AND (B AND C). [given]
  2. From A AND (B AND C): deduce (B AND C) AND A. [AND IS COMMUTATIVE]
  3. From (B AND C) AND A: deduce B AND (C AND A). [AND IS ASSOCIATIVE (left)]
  4. From B AND (C AND A): deduce (C AND A) AND B. [AND IS COMMUTATIVE]
  5. From (C AND A) AND B: deduce C AND (A AND B). [AND IS ASSOCIATIVE (left)]
  6. From C AND (A AND B): deduce (A AND B) AND C. [AND IS COMMUTATIVE]
  7. QED!
  • Some deductive rules use formulas (also known as well-formed formulas) as input.
  • Formulas look the same as statements, but whereas statements in the root environment are known to be true, a formula could be either true or false. As such, we place them in a separate Formulas window, which is now unlocked for use. For instance, in this exercise, the formulas B and C are not known to be true, but are still available for use in some rules of inference. The formula A is known to be true, so it can belong to both the Root environment and Formulas windows.
  • In mathematical logic, the logical connective OR (also known as disjunction) is interpreted as an inclusive or; the statement "A OR B" asserts that at least one of A and B are true, and in particular will remain true if both of A and B are true. This feature of OR is captured in part by the laws of disjunction introduction that have just been unlocked.
  • To use one of these laws, drag a formula from the Formulas window to a sentence in the Root environment window (or drag a sentence in the Root environment window to a formula in the Formulas window).
  • To apply this exercise to future exercises, one needs to select three hypotheses (A, Formula B, and Formula ) rather than just one or two. To do this, drag the first hypothesis to the second and then CTRL-click the third, or clicks the first and then CTRL-click the next two. Similarly for applying any other exercise with three or more hypotheses.
  1. A. [given]
  2. From A: deduce A OR B. [DISJUNCTION INTRODUCTION (left)]
  3. From A OR B: deduce C OR (A OR B). [DISJUNCTION INTRODUCTION (right)]
  4. QED!
OR IS IDEMPOTENT (left)
The reverse implication (deducing A from A OR A) is true, but will be deferred to Exercise 9.1(b), as we first need to introduce the important concept of an assumption and then introduce some further laws of disjunction.
  1. A. [given]
  2. From A: deduce A OR A. [DISJUNCTION INTRODUCTION (left)]
  3. QED!
  • The Root environment window holds all the statements that are known to be true under the given hypothesis. But sometimes in an argument, we also need to consider statements that are only conditionally known to be true, under one or more assumptions. For instance, we might not know that a statement A is true unconditionally, but instead know that A is conditionally true under the assumption of a second statement B.
  • In this interactive text, assumptions are depicted as subwindows of the Root environment window. For instance, to depict the knowledge of A conditionally under the assumption of B, one would form a subwindow of Root environment titled "Assume B", and place A inside that window.
  • The law of assumption (or implication introduction) asserts that if A is a formula, then it will be true if we first make an assumption that A holds.
  • Try dragging the formula A to the Root environment window (or clicking on the formula) to make such an assumption!
  • Every deductive rule that one can apply in the root environment, one can also apply in a sub-environment. This is the key to solving the current exercise (and to many subsequent exercises).
  1. Deduce A [assuming A]. [IMPLICATION INTRODUCTION]
  2. From A [assuming A], A [assuming A]: deduce A AND A [assuming A]. [CONJUNCTION INTRODUCTION]
  3. QED!
  • One can combine formulas together to create compound formulas.
  • For binary logical connectives such as AND and OR, this is done here by dragging formulas together in the Formulas window.
  • See what happens if one drags the formula A onto the formula B or vice versa!
  • For the purposes of recording proof length, the creation of new formulas is considered to be a "free move" in this text, in that it does not use up any lines of the proof.
  1. Deduce (A AND B) OR C [assuming (A AND B) OR C]. [IMPLICATION INTRODUCTION]
  2. QED!
  • Assumptions can be nested.
  • The statement "A, assuming B, A" asserts that if one assumes B, and then subsequently assumes A, then the statement A will be true under these two assumptions.
  • As with Exercise 4.1, the key to solving this exercise is in using the fact that any deductive rule that is applicable in the root environment, can also be applied in any sub-environment.
  1. Deduce B [assuming B]. [IMPLICATION INTRODUCTION]
  2. Deduce A [assuming B, A]. [IMPLICATION INTRODUCTION]
  3. QED!
IMPLIES IS IDEMPOTENT
  • The logical connective IMPLIES is also known as material implication (or the conditional); informally, one can think of the assertion IMPLIES(A, B) as the assertion that B is "at least as true as" A. (But they do not need to be equally true: in particular, if A is false and B is true, then it turns out that A IMPLIES B is true.
  • The statement A IMPLIES B can also be written as IF A, THEN B.
  • The deduction theorem asserts that if you can prove a statement B under the assumption of another statement A, then you can deduce the compound statement A IMPLIES B. It is very commonly used in mathematics to prove implication statements.
  • To use the deduction theorem, take a statement that is known under some hypothesis, and drag it out of the window corresponding to that hypothesis into the parent window. (In many cases, the parent window will be the Root environment window.)
  • In some proof systems for propositional calculus, the deduction theorem is not one of the given laws of inference, but actually has to be proven as a theorem, which explains the name. However, in this text, we will take the deduction theorem as a primitive inference rule.
  1. Deduce A [assuming A]. [IMPLICATION INTRODUCTION]
  2. From A [assuming A]: deduce A IMPLIES A. [DEDUCTION THEOREM]
  3. QED!
To prove an implication of the form X IMPLIES Y, first create X as a formula in the Formulas window, drag it to the Root environment window to use it as an assumption, and then try to establish Y inside the window corresponding to that assumption. Then use the deduction theorem.
  1. Deduce A AND (A OR B) [assuming A AND (A OR B)]. [IMPLICATION INTRODUCTION]
  2. From A AND (A OR B) [assuming A AND (A OR B)]: deduce A [assuming A AND (A OR B)]. [CONJUNCTION ELIMINATION (left)]
  3. From A [assuming A AND (A OR B)]: deduce (A AND (A OR B)) IMPLIES A. [DEDUCTION THEOREM]
  4. QED!
DOUBLE DEDUCTION THEOREM
  • This exercise easily follows from two applications of the deduction theorem, but is convenient for use in later exercises.
  • The appearance of [root environment] in the list of assumptions is not needed to solve the exercise; but it affects the user interface for applying the exercise. Namely, to invoke this theorem in the future, one should drag a statement "up" two levels, undoing two levels of assumption. (Without [root environment], one would instead click on the statement rather than drag it up two levels.)
  1. C [assuming A, B]. [given]
  2. From C [assuming A, B]: deduce B IMPLIES C [assuming A]. [DEDUCTION THEOREM]
  3. From B IMPLIES C [assuming A]: deduce A IMPLIES (B IMPLIES C). [DEDUCTION THEOREM]
  4. QED!
  • If a statement is known without an assumption, then it can be "pushed" into an enviroment with that assumption. For instance, if A is known to be true unconditionally, then it is also known to be true assuming B.
  • The push law is also known as "weakening" or monotonicity of entailment.
  • To apply a push, drag a statement into an assumption environment that shares the same parent environment as the original statement. (Alternatively, if this environment has not yet been created, drag the statement onto a formula containing the assumption, or vice versa.)
  1. Deduce A [assuming A]. [IMPLICATION INTRODUCTION]
  2. From A [assuming A]: deduce A [assuming A, B]. [PUSH (alternate form)]
  3. From A [assuming A, B]: deduce A IMPLIES (B IMPLIES A). [DOUBLE DEDUCTION THEOREM]
  4. QED!
DOUBLE PUSH
  • This exercise easily follows from two applications of the push law, but turns out to be convenient in some subsequent exercises.
  • The presence of the assumption environment [assuming B, C] is needed for two technical reasons. Firstly, it populates the formula window with the atomic formulas B, C, which otherwise would not be present. Secondly, it affects the user interface for applying the double push rule. Namely, to invoke this law, one should push a statement "down" two levels, into an assumption window that is two levels nested below the one that the statement lies in.
  • Thanks to Steve Trout for contributing a short proof.
  1. A. [given]
  2. From A: deduce A [assuming B]. [PUSH (alternate form)]
  3. From A [assuming B]: deduce A [assuming B, C]. [PUSH (alternate form)]
  4. QED!
MODUS PONENS (ASSUMPTION FORM)
  • Modus ponens is one of the most famous deductive rules. It asserts that if a statement A is known to be true, and it is also known that A IMPLIES B, then one can conclude that B is also true.
  • To apply this rule, drag the hypothesis A of an implication onto the implication A IMPLIES B. The two statements must lie in the same assumption window for the law to be applied.
  • Incidentally, this exercise (the "assumption" form of Modus ponens) is a useful tool for several subsequent exercises in this text, so keep it in mind. To apply this exercise, drag a hypothesis A to a conclusion B that has already been obtained under the assumption of A.
  1. A. [given]
  2. B [assuming A]. [given]
  3. From B [assuming A]: deduce A IMPLIES B. [DEDUCTION THEOREM]
  4. From A, A IMPLIES B: deduce B. [MODUS PONENS]
  5. QED!
REVERSE DEDUCTION THEOREM
This exercise will be useful in some later exercises. To apply it, click on an implication statement such as A IMPLIES B.
  1. A IMPLIES B. [given]
  2. Deduce A [assuming A]. [IMPLICATION INTRODUCTION]
  3. From A IMPLIES B: deduce A IMPLIES B [assuming A]. [PUSH]
  4. From A [assuming A], A IMPLIES B [assuming A]: deduce B [assuming A]. [MODUS PONENS]
  5. QED!
IMPLIES IS TRANSITIVE
  1. A IMPLIES B. [given]
  2. B IMPLIES C. [given]
  3. From A IMPLIES B: deduce B [assuming A]. [REVERSE DEDUCTION THEOREM]
  4. From B IMPLIES C: deduce B IMPLIES C [assuming A]. [PUSH]
  5. From B [assuming A], B IMPLIES C [assuming A]: deduce C [assuming A]. [MODUS PONENS]
  6. From C [assuming A]: deduce A IMPLIES C. [DEDUCTION THEOREM]
  7. QED!
AND IS COMMUTATIVE (implication form)
The fact that AND is commutative, proven in Exercise 2.1, will be helpful here.
  1. Deduce A AND B [assuming A AND B]. [IMPLICATION INTRODUCTION]
  2. From A AND B [assuming A AND B]: deduce B AND A [assuming A AND B]. [AND IS COMMUTATIVE]
  3. From B AND A [assuming A AND B]: deduce (A AND B) IMPLIES (B AND A). [DEDUCTION THEOREM]
  4. QED!
General tip: one can press "n" to advance to the next available unsolved exercise, or "N" to advance to the last available unsolved exercise (which will usually be the first exercise of the section after the last solved exercise).
  1. A IMPLIES (B IMPLIES C). [given]
  2. Deduce A AND B [assuming A AND B]. [IMPLICATION INTRODUCTION]
  3. From A AND B [assuming A AND B]: deduce A [assuming A AND B]. [CONJUNCTION ELIMINATION (left)]
  4. From A IMPLIES (B IMPLIES C): deduce A IMPLIES (B IMPLIES C) [assuming A AND B]. [PUSH]
  5. From A [assuming A AND B], A IMPLIES (B IMPLIES C) [assuming A AND B]: deduce B IMPLIES C [assuming A AND B]. [MODUS PONENS]
  6. From A AND B [assuming A AND B]: deduce B [assuming A AND B]. [CONJUNCTION ELIMINATION (right)]
  7. From B [assuming A AND B], B IMPLIES C [assuming A AND B]: deduce C [assuming A AND B]. [MODUS PONENS]
  8. From C [assuming A AND B]: deduce (A AND B) IMPLIES C. [DEDUCTION THEOREM]
  9. QED!
  1. (A AND B) IMPLIES C. [given]
  2. Deduce A [assuming A]. [IMPLICATION INTRODUCTION]
  3. Deduce B [assuming A, B]. [IMPLICATION INTRODUCTION]
  4. From A [assuming A]: deduce A [assuming A, B]. [PUSH]
  5. From A [assuming A, B], B [assuming A, B]: deduce A AND B [assuming A, B]. [CONJUNCTION INTRODUCTION]
  6. From (A AND B) IMPLIES C: deduce (A AND B) IMPLIES C [assuming A, B]. [DOUBLE PUSH]
  7. From A AND B [assuming A, B], (A AND B) IMPLIES C [assuming A, B]: deduce C [assuming A, B]. [MODUS PONENS]
  8. From C [assuming A, B]: deduce A IMPLIES (B IMPLIES C). [DOUBLE DEDUCTION THEOREM]
  9. QED!
Thanks to William Chargin and Junghyeon Park for a short proof.
  1. A IMPLIES (B IMPLIES C). [given]
  2. From A IMPLIES (B IMPLIES C): deduce (A AND B) IMPLIES C. [EXERCISE 8.4(a)]
  3. Deduce (B AND A) IMPLIES (A AND B). [EXERCISE 8.3]
  4. From (B AND A) IMPLIES (A AND B), (A AND B) IMPLIES C: deduce (B AND A) IMPLIES C. [IMPLIES IS TRANSITIVE]
  5. From (B AND A) IMPLIES C: deduce B IMPLIES (A IMPLIES C). [EXERCISE 8.4(b)]
  6. QED!
ABSORPTION (right)
  1. A IMPLIES B. [given]
  2. From A IMPLIES B: deduce B [assuming A]. [REVERSE DEDUCTION THEOREM]
  3. Deduce A [assuming A]. [IMPLICATION INTRODUCTION]
  4. From A [assuming A], B [assuming A]: deduce A AND B [assuming A]. [CONJUNCTION INTRODUCTION]
  5. From A AND B [assuming A]: deduce A IMPLIES (A AND B). [DEDUCTION THEOREM]
  6. QED!
ABSORPTION (left)
  1. A IMPLIES B. [given]
  2. From A IMPLIES B: deduce A IMPLIES (A AND B). [ABSORPTION (right)]
  3. Deduce (A AND B) IMPLIES (B AND A). [AND IS COMMUTATIVE (implication form)]
  4. From A IMPLIES (A AND B), (A AND B) IMPLIES (B AND A): deduce A IMPLIES (B AND A). [IMPLIES IS TRANSITIVE]
  5. QED!
  1. A AND B. [given]
  2. A IMPLIES C. [given]
  3. From A AND B: deduce A. [CONJUNCTION ELIMINATION (left)]
  4. From A AND B: deduce B. [CONJUNCTION ELIMINATION (right)]
  5. From A, A IMPLIES C: deduce C. [MODUS PONENS]
  6. From C, B: deduce C AND B. [CONJUNCTION INTRODUCTION]
  7. QED!
  1. A AND B. [given]
  2. B IMPLIES C. [given]
  3. From A AND B: deduce B AND A. [AND IS COMMUTATIVE]
  4. From B AND A, B IMPLIES C: deduce C AND A. [EXERCISE 8.6(a)]
  5. From C AND A: deduce A AND C. [AND IS COMMUTATIVE]
  6. QED!
OR IS COMMUTATIVE
  • We now return to the laws of disjunction (i.e., the laws of the "OR" connective).
  • To complement the laws of disjunction introduction from Section 3, one has the law of case analysis: if a statement C is known to be true under the assumption A, and also known to be true under the assumption B, then it is true under the assumption A OR B.
  • For instance, to solve the current exercise, first establish B OR A under the assumption of A, and then separately establish B OR A under the assumption of B. Then drag the two conclusions together!
  • Splitting into cases is a common technique in mathematics. For instance, to prove a statement A involving a natural number n, one might first prove the statement A assuming n is odd, and then prove it assuming n is even. Since n has to be odd or even, the law of case analysis then establishes the statement A unconditionally.
  1. A OR B. [given]
  2. Deduce A [assuming A]. [IMPLICATION INTRODUCTION]
  3. From A [assuming A]: deduce B OR A [assuming A]. [DISJUNCTION INTRODUCTION (right)]
  4. Deduce B [assuming B]. [IMPLICATION INTRODUCTION]
  5. From B [assuming B]: deduce B OR A [assuming B]. [DISJUNCTION INTRODUCTION (left)]
  6. From B OR A [assuming A], B OR A [assuming B]: deduce B OR A [assuming A OR B]. [CASE ANALYSIS]
  7. From A OR B, B OR A [assuming A OR B]: deduce B OR A. [MODUS PONENS (ASSUMPTION FORM)]
  8. QED!
OR IS IDEMPOTENT (right)
This is the reverse of Exercise 3.1(b).
  1. A OR A. [given]
  2. Deduce A [assuming A]. [IMPLICATION INTRODUCTION]
  3. From A [assuming A], A [assuming A]: deduce A [assuming A OR A]. [CASE ANALYSIS]
  4. From A OR A, A [assuming A OR A]: deduce A. [MODUS PONENS (ASSUMPTION FORM)]
  5. QED!
OR IS ASSOCIATIVE (left)
  • From this point onwards, the solutions will begin to be somewhat lengthy.
  • Thanks to Steve Trout, William Chargin, Daniel Spivak, and Keith Winstein for contributing a (relatively) short proof, and Anders Kaseorg for an even shorter proof.
  1. (A OR B) OR C. [given]
  2. Deduce A [assuming A]. [IMPLICATION INTRODUCTION]
  3. From A [assuming A]: deduce A OR (B OR C) [assuming A]. [DISJUNCTION INTRODUCTION (left)]
  4. Deduce B [assuming B]. [IMPLICATION INTRODUCTION]
  5. From B [assuming B]: deduce A OR (B OR C) [assuming B]. [EXERCISE 3.1(a)]
  6. Deduce C [assuming C]. [IMPLICATION INTRODUCTION]
  7. From C [assuming C]: deduce B OR C [assuming C]. [DISJUNCTION INTRODUCTION (right)]
  8. From B OR C [assuming C]: deduce A OR (B OR C) [assuming C]. [DISJUNCTION INTRODUCTION (right)]
  9. From A OR (B OR C) [assuming A], A OR (B OR C) [assuming B]: deduce A OR (B OR C) [assuming A OR B]. [CASE ANALYSIS]
  10. From A OR (B OR C) [assuming A OR B], A OR (B OR C) [assuming C]: deduce A OR (B OR C) [assuming (A OR B) OR C]. [CASE ANALYSIS]
  11. From (A OR B) OR C, A OR (B OR C) [assuming (A OR B) OR C]: deduce A OR (B OR C). [MODUS PONENS (ASSUMPTION FORM)]
  12. QED!
OR IS ASSOCIATIVE (right)
Thanks to William Chargin for a short proof.
  1. A OR (B OR C). [given]
  2. From A OR (B OR C): deduce (B OR C) OR A. [OR IS COMMUTATIVE]
  3. From (B OR C) OR A: deduce B OR (C OR A). [OR IS ASSOCIATIVE (left)]
  4. From B OR (C OR A): deduce (C OR A) OR B. [OR IS COMMUTATIVE]
  5. From (C OR A) OR B: deduce C OR (A OR B). [OR IS ASSOCIATIVE (left)]
  6. From C OR (A OR B): deduce (A OR B) OR C. [OR IS COMMUTATIVE]
  7. QED!
OR DISTRIBUTES OVER AND (left)
  1. A OR (B AND C). [given]
  2. Deduce A [assuming A]. [IMPLICATION INTRODUCTION]
  3. From A [assuming A]: deduce A OR B [assuming A]. [DISJUNCTION INTRODUCTION (left)]
  4. From A [assuming A]: deduce A OR C [assuming A]. [DISJUNCTION INTRODUCTION (left)]
  5. From A OR B [assuming A], A OR C [assuming A]: deduce (A OR B) AND (A OR C) [assuming A]. [CONJUNCTION INTRODUCTION]
  6. Deduce B AND C [assuming B AND C]. [IMPLICATION INTRODUCTION]
  7. From B AND C [assuming B AND C]: deduce B [assuming B AND C]. [CONJUNCTION ELIMINATION (left)]
  8. From B AND C [assuming B AND C]: deduce C [assuming B AND C]. [CONJUNCTION ELIMINATION (right)]
  9. From B [assuming B AND C]: deduce A OR B [assuming B AND C]. [DISJUNCTION INTRODUCTION (right)]
  10. From C [assuming B AND C]: deduce A OR C [assuming B AND C]. [DISJUNCTION INTRODUCTION (right)]
  11. From A OR B [assuming B AND C], A OR C [assuming B AND C]: deduce (A OR B) AND (A OR C) [assuming B AND C]. [CONJUNCTION INTRODUCTION]
  12. From (A OR B) AND (A OR C) [assuming A], (A OR B) AND (A OR C) [assuming B AND C]: deduce (A OR B) AND (A OR C) [assuming A OR (B AND C)]. [CASE ANALYSIS]
  13. From A OR (B AND C), (A OR B) AND (A OR C) [assuming A OR (B AND C)]: deduce (A OR B) AND (A OR C). [MODUS PONENS (ASSUMPTION FORM)]
  14. QED!
AND DISTRIBUTES OVER OR (left)
  1. A AND (B OR C). [given]
  2. From A AND (B OR C): deduce A. [CONJUNCTION ELIMINATION (left)]
  3. From A AND (B OR C): deduce B OR C. [CONJUNCTION ELIMINATION (right)]
  4. Deduce B [assuming B]. [IMPLICATION INTRODUCTION]
  5. From A: deduce A [assuming B]. [PUSH]
  6. From A [assuming B], B [assuming B]: deduce A AND B [assuming B]. [CONJUNCTION INTRODUCTION]
  7. From A AND B [assuming B]: deduce (A AND B) OR (A AND C) [assuming B]. [DISJUNCTION INTRODUCTION (left)]
  8. Deduce C [assuming C]. [IMPLICATION INTRODUCTION]
  9. From A: deduce A [assuming C]. [PUSH]
  10. From A [assuming C], C [assuming C]: deduce A AND C [assuming C]. [CONJUNCTION INTRODUCTION]
  11. From A AND C [assuming C]: deduce (A AND B) OR (A AND C) [assuming C]. [DISJUNCTION INTRODUCTION (right)]
  12. From (A AND B) OR (A AND C) [assuming B], (A AND B) OR (A AND C) [assuming C]: deduce (A AND B) OR (A AND C) [assuming B OR C]. [CASE ANALYSIS]
  13. From B OR C, (A AND B) OR (A AND C) [assuming B OR C]: deduce (A AND B) OR (A AND C). [MODUS PONENS (ASSUMPTION FORM)]
  14. QED!
AND DISTRIBUTES OVER OR (right)
  1. (A AND B) OR (A AND C). [given]
  2. Deduce A AND B [assuming A AND B]. [IMPLICATION INTRODUCTION]
  3. From A AND B [assuming A AND B]: deduce A [assuming A AND B]. [CONJUNCTION ELIMINATION (left)]
  4. From A AND B [assuming A AND B]: deduce B [assuming A AND B]. [CONJUNCTION ELIMINATION (right)]
  5. From B [assuming A AND B]: deduce B OR C [assuming A AND B]. [DISJUNCTION INTRODUCTION (left)]
  6. From A [assuming A AND B], B OR C [assuming A AND B]: deduce A AND (B OR C) [assuming A AND B]. [CONJUNCTION INTRODUCTION]
  7. Deduce A AND C [assuming A AND C]. [IMPLICATION INTRODUCTION]
  8. From A AND C [assuming A AND C]: deduce A [assuming A AND C]. [CONJUNCTION ELIMINATION (left)]
  9. From A AND C [assuming A AND C]: deduce C [assuming A AND C]. [CONJUNCTION ELIMINATION (right)]
  10. From C [assuming A AND C]: deduce B OR C [assuming A AND C]. [DISJUNCTION INTRODUCTION (right)]
  11. From A [assuming A AND C], B OR C [assuming A AND C]: deduce A AND (B OR C) [assuming A AND C]. [CONJUNCTION INTRODUCTION]
  12. From A AND (B OR C) [assuming A AND B], A AND (B OR C) [assuming A AND C]: deduce A AND (B OR C) [assuming (A AND B) OR (A AND C)]. [CASE ANALYSIS]
  13. From (A AND B) OR (A AND C), A AND (B OR C) [assuming (A AND B) OR (A AND C)]: deduce A AND (B OR C). [MODUS PONENS (ASSUMPTION FORM)]
  14. QED!
OR DISTRIBUTES OVER AND (right)
Thanks to Jan Wieners for the short proof.
  1. (A OR B) AND (A OR C). [given]
  2. Deduce B [assuming B]. [IMPLICATION INTRODUCTION]
  3. From (A OR B) AND (A OR C): deduce A OR C. [CONJUNCTION ELIMINATION (right)]
  4. From A OR C: deduce A OR C [assuming B]. [PUSH]
  5. From B [assuming B], A OR C [assuming B]: deduce B AND (A OR C) [assuming B]. [CONJUNCTION INTRODUCTION]
  6. From B AND (A OR C) [assuming B]: deduce (B AND A) OR (B AND C) [assuming B]. [AND DISTRIBUTES OVER OR (left)]
  7. Deduce A [assuming A]. [IMPLICATION INTRODUCTION]
  8. From A [assuming A]: deduce A OR (B AND C) [assuming A]. [DISJUNCTION INTRODUCTION (left)]
  9. From (B AND A) OR (B AND C) [assuming B]: deduce (B AND C) OR (B AND A) [assuming B]. [OR IS COMMUTATIVE]
  10. From (B AND C) OR (B AND A) [assuming B]: deduce ((B AND C) OR B) AND ((B AND C) OR A) [assuming B]. [OR DISTRIBUTES OVER AND (left)]
  11. From ((B AND C) OR B) AND ((B AND C) OR A) [assuming B]: deduce (B AND C) OR A [assuming B]. [CONJUNCTION ELIMINATION (right)]
  12. From (B AND C) OR A [assuming B]: deduce A OR (B AND C) [assuming B]. [OR IS COMMUTATIVE]
  13. From A OR (B AND C) [assuming A], A OR (B AND C) [assuming B]: deduce A OR (B AND C) [assuming A OR B]. [CASE ANALYSIS]
  14. From (A OR B) AND (A OR C): deduce A OR B. [CONJUNCTION ELIMINATION (left)]
  15. From A OR B, A OR (B AND C) [assuming A OR B]: deduce A OR (B AND C). [MODUS PONENS (ASSUMPTION FORM)]
  16. QED!
CONSTRUCTIVE DILEMMA (left)
  1. A OR B. [given]
  2. A IMPLIES C. [given]
  3. From A IMPLIES C: deduce C [assuming A]. [REVERSE DEDUCTION THEOREM]
  4. From C [assuming A]: deduce C OR B [assuming A]. [DISJUNCTION INTRODUCTION (left)]
  5. Deduce B [assuming B]. [IMPLICATION INTRODUCTION]
  6. From B [assuming B]: deduce C OR B [assuming B]. [DISJUNCTION INTRODUCTION (right)]
  7. From C OR B [assuming A], C OR B [assuming B]: deduce C OR B [assuming A OR B]. [CASE ANALYSIS]
  8. From A OR B, C OR B [assuming A OR B]: deduce C OR B. [MODUS PONENS (ASSUMPTION FORM)]
  9. QED!
CONSTRUCTIVE DILEMMA (right)
Thanks to William Chargin for a short proof.
  1. A OR B. [given]
  2. B IMPLIES C. [given]
  3. From A OR B: deduce B OR A. [OR IS COMMUTATIVE]
  4. From B OR A, B IMPLIES C: deduce C OR A. [CONSTRUCTIVE DILEMMA (left)]
  5. From C OR A: deduce A OR C. [OR IS COMMUTATIVE]
  6. QED!
CONSTRUCTIVE DILEMMA (both)
  • This exercise involves three hypotheses, so it cannot be directly invoked by clicking or dragging on these hypotheses. However, if one drags the first hypothesis to the second and then CTRL-clicks the third, or if one clicks the first and then CTRL-clicks the next two, one will be able to apply this exercise (once it is proven), of course. Alternatively, one can use the two halves of this dilemma in Exercise 19(a) and Exercise 19(b) as a substitute.
  • This exercise can be solved quickly if one uses Exercises 9.4(a) and 9.4(b). (Of course, you must then solve these exercises first!)
  1. A OR B. [given]
  2. A IMPLIES C. [given]
  3. B IMPLIES D. [given]
  4. From A OR B, A IMPLIES C: deduce C OR B. [CONSTRUCTIVE DILEMMA (left)]
  5. From C OR B, B IMPLIES D: deduce C OR D. [CONSTRUCTIVE DILEMMA (right)]
  6. QED!
MONOTONICITY OF AND (right)
Thanks to dP dt for the short proof, and Anders Kaseorg for a shorter proof (located using computer search!).
  1. A IMPLIES B. [given]
  2. Deduce (B AND C) IMPLIES (B AND C). [IMPLIES IS IDEMPOTENT]
  3. From (B AND C) IMPLIES (B AND C): deduce B IMPLIES (C IMPLIES (B AND C)). [EXERCISE 8.4(b)]
  4. From A IMPLIES B, B IMPLIES (C IMPLIES (B AND C)): deduce A IMPLIES (C IMPLIES (B AND C)). [IMPLIES IS TRANSITIVE]
  5. From A IMPLIES (C IMPLIES (B AND C)): deduce (A AND C) IMPLIES (B AND C). [EXERCISE 8.4(a)]
  6. QED!
MONOTONICITY OF OR (right)
Thanks to Pace Nielsen, Andrew Liftin, Alan Lu, and Ephim Kolmogorov for the short proof.
  1. A IMPLIES B. [given]
  2. Deduce A OR C [assuming A OR C]. [IMPLICATION INTRODUCTION]
  3. From A IMPLIES B: deduce A IMPLIES B [assuming A OR C]. [PUSH]
  4. From A OR C [assuming A OR C], A IMPLIES B [assuming A OR C]: deduce B OR C [assuming A OR C]. [CONSTRUCTIVE DILEMMA (left)]
  5. From B OR C [assuming A OR C]: deduce (A OR C) IMPLIES (B OR C). [DEDUCTION THEOREM]
  6. QED!
MONOTONICITY OF AND (left)
Thanks to Gesse Roure for a short proof.
  1. A IMPLIES B. [given]
  2. Deduce C AND A [assuming C AND A]. [IMPLICATION INTRODUCTION]
  3. From A IMPLIES B: deduce A IMPLIES B [assuming C AND A]. [PUSH]
  4. From C AND A [assuming C AND A], A IMPLIES B [assuming C AND A]: deduce C AND B [assuming C AND A]. [EXERCISE 8.6(b)]
  5. From C AND B [assuming C AND A]: deduce (C AND A) IMPLIES (C AND B). [DEDUCTION THEOREM]
  6. QED!
MONOTONICITY OF OR (left)
  1. A IMPLIES B. [given]
  2. Deduce C OR A [assuming C OR A]. [IMPLICATION INTRODUCTION]
  3. From A IMPLIES B: deduce A IMPLIES B [assuming C OR A]. [PUSH]
  4. From C OR A [assuming C OR A], A IMPLIES B [assuming C OR A]: deduce C OR B [assuming C OR A]. [CONSTRUCTIVE DILEMMA (right)]
  5. From C OR B [assuming C OR A]: deduce (C OR A) IMPLIES (C OR B). [DEDUCTION THEOREM]
  6. QED!
SUBSTITUTION
  • The logical connective IFF (short for "IF AND ONLY IF") is also known as the biconditional.
  • As the laws of biconditional assert, the statement A IFF B is equivalent to the statements A IMPLIES B and B IMPLIES A both being true.
  • Another way of thinking about it is that the statement A IFF B asserts that A and B are equally true.
  • To use the laws, either click on a statement of the form A IFF B to be able to apply biconditional elimination to deduce A IMPLIES B or B IMPLIES A, or drag A IMPLIES B and B IMPLIES A together to form A IFF B (or B IFF A) via the law of biconditional introduction.
  1. A. [given]
  2. A IFF B. [given]
  3. From A IFF B: deduce A IMPLIES B. [BICONDITIONAL ELIMINATION (left)]
  4. From A, A IMPLIES B: deduce B. [MODUS PONENS]
  5. QED!
SUBSTITUTION FOR AND (left)
Thanks to Wilson Cheang and Alan Lu for a short proof from a previous version of the text.
  1. A AND B. [given]
  2. A IFF C. [given]
  3. From A IFF C: deduce A IMPLIES C. [BICONDITIONAL ELIMINATION (left)]
  4. From A AND B, A IMPLIES C: deduce C AND B. [EXERCISE 8.6(a)]
  5. QED!
SUBSTITUTION FOR AND (right)
  1. A AND B. [given]
  2. B IFF C. [given]
  3. From B IFF C: deduce B IMPLIES C. [BICONDITIONAL ELIMINATION (left)]
  4. From A AND B, B IMPLIES C: deduce A AND C. [EXERCISE 8.6(b)]
  5. QED!
SUBSTITUTION FOR OR (left)
  1. A OR B. [given]
  2. A IFF C. [given]
  3. From A IFF C: deduce A IMPLIES C. [BICONDITIONAL ELIMINATION (left)]
  4. From A OR B, A IMPLIES C: deduce C OR B. [CONSTRUCTIVE DILEMMA (left)]
  5. QED!
SUBSTITUTION FOR OR (right)
  1. A OR B. [given]
  2. B IFF C. [given]
  3. From B IFF C: deduce B IMPLIES C. [BICONDITIONAL ELIMINATION (left)]
  4. From A OR B, B IMPLIES C: deduce A OR C. [CONSTRUCTIVE DILEMMA (right)]
  5. QED!
SUBSTITUTION FOR IMPLIES (left)
  1. A IMPLIES B. [given]
  2. A IFF C. [given]
  3. From A IFF C: deduce C IMPLIES A. [BICONDITIONAL ELIMINATION (right)]
  4. From C IMPLIES A, A IMPLIES B: deduce C IMPLIES B. [IMPLIES IS TRANSITIVE]
  5. QED!
SUBSTITUTION FOR IMPLIES (right)
  1. A IMPLIES B. [given]
  2. B IFF C. [given]
  3. From B IFF C: deduce B IMPLIES C. [BICONDITIONAL ELIMINATION (left)]
  4. From A IMPLIES B, B IMPLIES C: deduce A IMPLIES C. [IMPLIES IS TRANSITIVE]
  5. QED!
IFF IS SYMMETRIC
  1. A IFF B. [given]
  2. From A IFF B: deduce A IMPLIES B. [BICONDITIONAL ELIMINATION (left)]
  3. From A IFF B: deduce B IMPLIES A. [BICONDITIONAL ELIMINATION (right)]
  4. From B IMPLIES A, A IMPLIES B: deduce B IFF A. [BICONDITIONAL INTRODUCTION]
  5. QED!
IFF IS TRANSITIVE
  1. A IFF B. [given]
  2. B IFF C. [given]
  3. From A IFF B: deduce A IMPLIES B. [BICONDITIONAL ELIMINATION (left)]
  4. From A IMPLIES B, B IFF C: deduce A IMPLIES C. [SUBSTITUTION FOR IMPLIES (right)]
  5. From A IFF B: deduce B IMPLIES A. [BICONDITIONAL ELIMINATION (right)]
  6. From B IMPLIES A, B IFF C: deduce C IMPLIES A. [SUBSTITUTION FOR IMPLIES (left)]
  7. From A IMPLIES C, C IMPLIES A: deduce A IFF C. [BICONDITIONAL INTRODUCTION]
  8. QED!
IFF IS REFLEXIVE
"if it was so, it might be; and if it were so, it would be; but as it isn't, it ain't. That's logic." - Tweedledee, "Through the Looking Glass"
  • The facts that IFF is symmetric, transitive, and reflexive can be combined into the single assertion that IFF is an equivalence relation.
  1. Deduce A IMPLIES A. [IMPLIES IS IDEMPOTENT]
  2. From A IMPLIES A, A IMPLIES A: deduce A IFF A. [BICONDITIONAL INTRODUCTION]
  3. QED!
BICONDITIONAL INTRODUCTION (ASSUMPTION FORM)
This form of biconditional introduction is convenient in some later exercises, as it can shorten proofs slightly.
  1. A [assuming B]. [given]
  2. B [assuming A]. [given]
  3. From A [assuming B]: deduce B IMPLIES A. [DEDUCTION THEOREM]
  4. From B [assuming A]: deduce A IMPLIES B. [DEDUCTION THEOREM]
  5. From A IMPLIES B, B IMPLIES A: deduce A IFF B. [BICONDITIONAL INTRODUCTION]
  6. QED!
OR IS IDEMPOTENT (biconditional form)
  • The left and right idempotence of OR, proven in Exercise 3.1(b) and Exercise 9.1(b) respectively, will be useful here.
  • Thanks to Chen Xu and JP Sugarbroad for the short proof.
  1. Deduce A [assuming A]. [IMPLICATION INTRODUCTION]
  2. From A [assuming A], A [assuming A]: deduce A [assuming A OR A]. [CASE ANALYSIS]
  3. From A [assuming A]: deduce A OR A [assuming A]. [DISJUNCTION INTRODUCTION (left)]
  4. From A [assuming A OR A], A OR A [assuming A]: deduce A IFF (A OR A). [BICONDITIONAL INTRODUCTION (ASSUMPTION FORM)]
  5. QED!
AND IS ASSOCIATIVE (biconditional form)
The fact that AND is associative, proven in Exercise 2.2(a) and Exercise 2.2(b) will be useful here.
  1. Deduce (A AND B) AND C [assuming (A AND B) AND C]. [IMPLICATION INTRODUCTION]
  2. From (A AND B) AND C [assuming (A AND B) AND C]: deduce A AND (B AND C) [assuming (A AND B) AND C]. [AND IS ASSOCIATIVE (left)]
  3. Deduce A AND (B AND C) [assuming A AND (B AND C)]. [IMPLICATION INTRODUCTION]
  4. From A AND (B AND C) [assuming A AND (B AND C)]: deduce (A AND B) AND C [assuming A AND (B AND C)]. [AND IS ASSOCIATIVE (right)]
  5. From (A AND B) AND C [assuming A AND (B AND C)], A AND (B AND C) [assuming (A AND B) AND C]: deduce ((A AND B) AND C) IFF (A AND (B AND C)). [BICONDITIONAL INTRODUCTION (ASSUMPTION FORM)]
  6. QED!
EX FALSO QUODLIBET
"When you have eliminated the impossible, whatever remains, however improbable, must be the truth" - Sherlock Holmes, "The Sign of the Four".
  • The logical connective NOT (also known as negation) is a unary connective; click on a formula to find the option to build the negated formula. A statement NOT A is true when A is false, and false when A is true.
  • We have unlocked the laws of disjunctive elimination. These laws assert that if a disjunction A OR B is true, and (say) NOT A is known to be true (so A is known to be false), then B must be true.
  • To use this law, drag a disjunction such as A OR B to the negation of either A or B; one can also drag in the reversed direction.
  • This exercise, ex falso quodlibet, is also known as the "principle of explosion". Informally, it asserts that once one has arrived at a contradiction, one can obtain any conclusion one wishes.
  • To apply ex falso quodlibet in subsequent exercises, drag a sentence of the form A AND (NOT A) to a formula in the Formulas window (or vice versa).
  1. A AND (NOT A). [given]
  2. From A AND (NOT A): deduce A. [CONJUNCTION ELIMINATION (left)]
  3. From A AND (NOT A): deduce NOT A. [CONJUNCTION ELIMINATION (right)]
  4. From A: deduce A OR B. [DISJUNCTION INTRODUCTION (left)]
  5. From A OR B, NOT A: deduce B. [DISJUNCTIVE ELIMINATION (left)]
  6. QED!
EX FALSO QUODLIBET (reversed)
  1. (NOT A) AND A. [given]
  2. From (NOT A) AND A: deduce A AND (NOT A). [AND IS COMMUTATIVE]
  3. From A AND (NOT A): deduce B. [EX FALSO QUODLIBET]
  4. QED!
REDUCTIO AD ABSURDUM
  • The law of the excluded middle is one of the most powerful rules in classical propositional logic, playing a role somewhat analogous to that of the parallel postulate in Euclidean geometry; it completes the basic set of rules of inference for propositional logic.
  • The law asserts that for any statement A, one of the statements A and NOT A is true. To apply this law, drag the formula A from the Formulas window to an assumption environment (such as the Root environment), or just click on A if one wants to use the law in the root environment.
  • If one removes the law of the excluded middle from classical logic (replacing it with the reductio ad absurdum rule of this exercise), one obtains the system of constructivist logic (also known as intuitionistic logic), which is deductively weaker, but (by the same token) makes a stronger assertion about the statements that it can still prove.
  • Reductio ad absurdum is a far finer gambit than any chess gambit: a chess player may offer the sacrifice of a pawn or even a piece, but a mathematician offers the game. - G. H. Hardy
  1. B AND (NOT B) [assuming A]. [given]
  2. From B AND (NOT B) [assuming A]: deduce NOT A [assuming A]. [EX FALSO QUODLIBET]
  3. Deduce NOT A [assuming NOT A]. [IMPLICATION INTRODUCTION]
  4. From NOT A [assuming A], NOT A [assuming NOT A]: deduce NOT A [assuming A OR (NOT A)]. [CASE ANALYSIS]
  5. Deduce A OR (NOT A). [EXCLUDED MIDDLE]
  6. From A OR (NOT A), NOT A [assuming A OR (NOT A)]: deduce NOT A. [MODUS PONENS (ASSUMPTION FORM)]
  7. QED!
REDUCTIO AD ABSURDUM (separated form)
  • This form of reductio ad absurdum is slightly more convenient to use in subsequent exercises. To apply it, combine B and NOT B together inside an assumption environment.
  1. B [assuming A]. [given]
  2. NOT B [assuming A]. [given]
  3. From B [assuming A], NOT B [assuming A]: deduce B AND (NOT B) [assuming A]. [CONJUNCTION INTRODUCTION]
  4. From B AND (NOT B) [assuming A]: deduce NOT A. [REDUCTIO AD ABSURDUM]
  5. QED!
EXCLUDED MIDDLE (case analysis form)
  • This form of the excluded middle is slightly more convenient to use in subsequent exercises. To apply it, combine a statement B (in a window assuming some formula A) with the same statement B (in a separate window assuming NOT A).
  1. B [assuming A]. [given]
  2. B [assuming NOT A]. [given]
  3. From B [assuming A], B [assuming NOT A]: deduce B [assuming A OR (NOT A)]. [CASE ANALYSIS]
  4. Deduce A OR (NOT A). [EXCLUDED MIDDLE]
  5. From A OR (NOT A), B [assuming A OR (NOT A)]: deduce B. [MODUS PONENS (ASSUMPTION FORM)]
  6. QED!
EXCLUDED MIDDLE (reversed form)
  1. Deduce A OR (NOT A). [EXCLUDED MIDDLE]
  2. From A OR (NOT A): deduce (NOT A) OR A. [OR IS COMMUTATIVE]
  3. QED!
DOUBLE NEGATION (right)
  1. NOT (NOT A). [given]
  2. Deduce A OR (NOT A). [EXCLUDED MIDDLE]
  3. From A OR (NOT A), NOT (NOT A): deduce A. [DISJUNCTIVE ELIMINATION (right)]
  4. QED!
DOUBLE NEGATION (left)
Thanks to Steve Trout, Hugo Musso Gualandi, Jon Easterday, William Chargin, Haggai Nuchi, Andrew Lei, Jim Apple, Jorge Cañizales Díaz, and Matthew Steffen for discovering the short proof.
  1. A. [given]
  2. Deduce NOT A [assuming NOT A]. [IMPLICATION INTRODUCTION]
  3. From A: deduce A [assuming NOT A]. [PUSH]
  4. From A [assuming NOT A], NOT A [assuming NOT A]: deduce NOT (NOT A). [REDUCTIO AD ABSURDUM (separated form)]
  5. QED!
DOUBLE NEGATION (both)
  1. Deduce A [assuming A]. [IMPLICATION INTRODUCTION]
  2. From A [assuming A]: deduce NOT (NOT A) [assuming A]. [DOUBLE NEGATION (left)]
  3. Deduce NOT (NOT A) [assuming NOT (NOT A)]. [IMPLICATION INTRODUCTION]
  4. From NOT (NOT A) [assuming NOT (NOT A)]: deduce A [assuming NOT (NOT A)]. [DOUBLE NEGATION (right)]
  5. From A [assuming NOT (NOT A)], NOT (NOT A) [assuming A]: deduce A IFF (NOT (NOT A)). [BICONDITIONAL INTRODUCTION (ASSUMPTION FORM)]
  6. QED!
PROOF BY CONTRADICTION
Thanks to Tyler Freeman and Chandler Watson for a short proof, and Hugo Musso Gualandi, Jon Easterday, Haggai Nuchi, and Jorge Cañizales Díaz for an even shorter proof.
  1. B AND (NOT B) [assuming NOT A]. [given]
  2. From B AND (NOT B) [assuming NOT A]: deduce NOT (NOT A). [REDUCTIO AD ABSURDUM]
  3. From NOT (NOT A): deduce A. [DOUBLE NEGATION (right)]
  4. QED!
PROOF BY CONTRADICTION (reversed form)
  1. (NOT B) AND B [assuming NOT A]. [given]
  2. From (NOT B) AND B [assuming NOT A]: deduce B AND (NOT B) [assuming NOT A]. [AND IS COMMUTATIVE]
  3. From B AND (NOT B) [assuming NOT A]: deduce A. [PROOF BY CONTRADICTION]
  4. QED!
Thanks to Anders Kaseorg and Carl Lucas for a short proof.
  1. A IMPLIES B. [given]
  2. Deduce (NOT A) OR A. [EXCLUDED MIDDLE (reversed form)]
  3. From (NOT A) OR A, A IMPLIES B: deduce (NOT A) OR B. [CONSTRUCTIVE DILEMMA (right)]
  4. QED!
Thanks to Yuval Wigderson, cory, Tyler Freeman, Haggai Nuchi, and Chandler Watson for supplying the short proof for this exercise.
  1. (NOT A) OR B. [given]
  2. Deduce A [assuming A]. [IMPLICATION INTRODUCTION]
  3. From (NOT A) OR B: deduce (NOT A) OR B [assuming A]. [PUSH]
  4. From A [assuming A]: deduce NOT (NOT A) [assuming A]. [DOUBLE NEGATION (left)]
  5. From (NOT A) OR B [assuming A], NOT (NOT A) [assuming A]: deduce B [assuming A]. [DISJUNCTIVE ELIMINATION (left)]
  6. From B [assuming A]: deduce A IMPLIES B. [DEDUCTION THEOREM]
  7. QED!
  1. Deduce A IMPLIES B [assuming A IMPLIES B]. [IMPLICATION INTRODUCTION]
  2. From A IMPLIES B [assuming A IMPLIES B]: deduce (NOT A) OR B [assuming A IMPLIES B]. [EXERCISE 12.4(a)]
  3. Deduce (NOT A) OR B [assuming (NOT A) OR B]. [IMPLICATION INTRODUCTION]
  4. From (NOT A) OR B [assuming (NOT A) OR B]: deduce A IMPLIES B [assuming (NOT A) OR B]. [EXERCISE 12.4(b)]
  5. From A IMPLIES B [assuming (NOT A) OR B], (NOT A) OR B [assuming A IMPLIES B]: deduce (A IMPLIES B) IFF ((NOT A) OR B). [BICONDITIONAL INTRODUCTION (ASSUMPTION FORM)]
  6. QED!
DE MORGAN'S LAW I
Thanks to Daniel Spivak for a short proof.
  1. NOT (A OR B). [given]
  2. Deduce A [assuming A]. [IMPLICATION INTRODUCTION]
  3. From A [assuming A]: deduce A OR B [assuming A]. [DISJUNCTION INTRODUCTION (left)]
  4. From NOT (A OR B): deduce NOT (A OR B) [assuming A]. [PUSH]
  5. From A OR B [assuming A], NOT (A OR B) [assuming A]: deduce NOT A. [REDUCTIO AD ABSURDUM (separated form)]
  6. Deduce B [assuming B]. [IMPLICATION INTRODUCTION]
  7. From B [assuming B]: deduce A OR B [assuming B]. [DISJUNCTION INTRODUCTION (right)]
  8. From NOT (A OR B): deduce NOT (A OR B) [assuming B]. [PUSH]
  9. From A OR B [assuming B], NOT (A OR B) [assuming B]: deduce NOT B. [REDUCTIO AD ABSURDUM (separated form)]
  10. From NOT A, NOT B: deduce (NOT A) AND (NOT B). [CONJUNCTION INTRODUCTION]
  11. QED!
DE MORGAN'S LAW II
Thanks to Anders Kaseorg for a short proof (found by computer search!).
  1. (NOT A) OR (NOT B). [given]
  2. From (NOT A) OR (NOT B): deduce A IMPLIES (NOT B). [EXERCISE 12.4(b)]
  3. From A IMPLIES (NOT B): deduce (A AND B) IMPLIES ((NOT B) AND B). [MONOTONICITY OF AND]
  4. From (A AND B) IMPLIES ((NOT B) AND B): deduce (NOT B) AND B [assuming A AND B]. [REVERSE DEDUCTION THEOREM]
  5. From (NOT B) AND B [assuming A AND B]: deduce B AND (NOT B) [assuming A AND B]. [AND IS COMMUTATIVE]
  6. From B AND (NOT B) [assuming A AND B]: deduce NOT (A AND B). [REDUCTIO AD ABSURDUM]
  7. QED!
DE MORGAN'S LAW III
Thanks to Daniel Spivak, Anders Kaseorg, Vincent Hwang, and Olle Wiklund for supplying the short proof for this exercise.
  1. NOT (A AND B). [given]
  2. Deduce A [assuming A]. [IMPLICATION INTRODUCTION]
  3. Deduce B [assuming A, B]. [IMPLICATION INTRODUCTION]
  4. From A [assuming A]: deduce A [assuming A, B]. [PUSH]
  5. From A [assuming A, B], B [assuming A, B]: deduce A AND B [assuming A, B]. [CONJUNCTION INTRODUCTION]
  6. From NOT (A AND B): deduce NOT (A AND B) [assuming A, B]. [DOUBLE PUSH]
  7. From A AND B [assuming A, B], NOT (A AND B) [assuming A, B]: deduce NOT B [assuming A]. [REDUCTIO AD ABSURDUM (separated form)]
  8. From NOT B [assuming A]: deduce A IMPLIES (NOT B). [DEDUCTION THEOREM]
  9. From A IMPLIES (NOT B): deduce (NOT A) OR (NOT B). [EXERCISE 12.4(a)]
  10. QED!
DE MORGAN'S LAW IV
Object Dual
TRUE FALSE
AND OR
NOT NOT
FOR ALL THERE EXISTS
Hypothesis Conclusion
  • At this point, the reader may have noticed a certain symmetry to propositional logic. This symmetry is formalised by the duality principle in boolean algebra, and may be summarised by the displayed table of "dual" pairs.
  • Every deductive law involving the connectives TRUE, FALSE, AND, OR, and NOT with a single hypothesis and conclusion then has a dual law in which the hypothesis and conclusion are interchanged, and the logical connectives are replaced with their duals as indicated by the table.
  • For instance, Exercise 12.5(a) and Exercise 12.5(b) are dual, as are Exercise 12.5(c) and Exercise 12.5(d).
  • Thanks to Yuval Wigderson and cory for supplying the short proof for this exercise.
  1. (NOT A) AND (NOT B). [given]
  2. Deduce A OR B [assuming A OR B]. [IMPLICATION INTRODUCTION]
  3. From (NOT A) AND (NOT B): deduce (NOT A) AND (NOT B) [assuming A OR B]. [PUSH]
  4. From (NOT A) AND (NOT B) [assuming A OR B]: deduce NOT A [assuming A OR B]. [CONJUNCTION ELIMINATION (left)]
  5. From (NOT A) AND (NOT B) [assuming A OR B]: deduce NOT B [assuming A OR B]. [CONJUNCTION ELIMINATION (right)]
  6. From A OR B [assuming A OR B], NOT A [assuming A OR B]: deduce B [assuming A OR B]. [DISJUNCTIVE ELIMINATION (left)]
  7. From B [assuming A OR B], NOT B [assuming A OR B]: deduce NOT (A OR B). [REDUCTIO AD ABSURDUM (separated form)]
  8. QED!
CONTRAPOSITION
  • Contraposition is also known as transposition, and the statement (NOT B) IMPLIES (NOT A) is known as the contrapositive of A IMPLIES B.
  • Thanks to Steve Trout for a short proof, and Andrew Litfin and Andrew Lei for a shorter proof.
  1. A IMPLIES B. [given]
  2. Deduce NOT B [assuming NOT B]. [IMPLICATION INTRODUCTION]
  3. From A IMPLIES B: deduce A IMPLIES B [assuming NOT B]. [PUSH]
  4. From A IMPLIES B [assuming NOT B]: deduce (NOT A) OR B [assuming NOT B]. [EXERCISE 12.4(a)]
  5. From (NOT A) OR B [assuming NOT B], NOT B [assuming NOT B]: deduce NOT A [assuming NOT B]. [DISJUNCTIVE ELIMINATION (right)]
  6. From NOT A [assuming NOT B]: deduce (NOT B) IMPLIES (NOT A). [DEDUCTION THEOREM]
  7. QED!
MODUS TOLLENS
  1. A IMPLIES B. [given]
  2. NOT B. [given]
  3. From A IMPLIES B: deduce (NOT B) IMPLIES (NOT A). [CONTRAPOSITION]
  4. From NOT B, (NOT B) IMPLIES (NOT A): deduce NOT A. [MODUS PONENS]
  5. QED!
SUBSTITUTION FOR NOT
Thanks to Haggai Nuchi for a short proof, and Tyler Freeman, Jim Apple, and Jorge Cañizales Díaz for an even shorter proof.
  1. NOT A. [given]
  2. A IFF B. [given]
  3. From A IFF B: deduce B IMPLIES A. [BICONDITIONAL ELIMINATION (right)]
  4. From B IMPLIES A, NOT A: deduce NOT B. [MODUS TOLLENS]
  5. QED!
MODUS TOLLENS (alternate form)
Thanks to Brian Quach for suggesting this exercise.
  1. A IMPLIES (NOT B). [given]
  2. B. [given]
  3. From B: deduce NOT (NOT B). [DOUBLE NEGATION (left)]
  4. From A IMPLIES (NOT B), NOT (NOT B): deduce NOT A. [MODUS TOLLENS]
  5. QED!
PEIRCE'S LAW
  1. (A IMPLIES B) IMPLIES A. [given]
  2. Deduce NOT A [assuming NOT A]. [IMPLICATION INTRODUCTION]
  3. From NOT A [assuming NOT A]: deduce (NOT A) OR B [assuming NOT A]. [DISJUNCTION INTRODUCTION (left)]
  4. From (NOT A) OR B [assuming NOT A]: deduce A IMPLIES B [assuming NOT A]. [EXERCISE 12.4(b)]
  5. From (A IMPLIES B) IMPLIES A: deduce (A IMPLIES B) IMPLIES A [assuming NOT A]. [PUSH]
  6. From A IMPLIES B [assuming NOT A], (A IMPLIES B) IMPLIES A [assuming NOT A]: deduce A [assuming NOT A]. [MODUS PONENS]
  7. From A [assuming NOT A], NOT A [assuming NOT A]: deduce NOT (NOT A). [REDUCTIO AD ABSURDUM (separated form)]
  8. From NOT (NOT A): deduce A. [DOUBLE NEGATION (right)]
  9. QED!
RESOLUTION
  1. A OR B. [given]
  2. (NOT A) OR C. [given]
  3. From (NOT A) OR C: deduce A IMPLIES C. [EXERCISE 12.4(b)]
  4. From A OR B, A IMPLIES C: deduce C OR B. [CONSTRUCTIVE DILEMMA (left)]
  5. QED!
TRUE IS IDENTITY FOR AND
  • In propositional logic, there are two formulas with a constant truth value: TRUE, which is always true, and FALSE, which is never true. These have now been permanently added to the Formulas window for use.
  • There is just one law for TRUE: TRUE is always true! To use it, drag TRUE from the Formulas window to any environment (or just click on TRUE, if one wants to create it in the root environment).
  • Similarly, there is one law for FALSE, namely that NOT(FALSE) is always true. To use it, create the formula NOT FALSE in the Formulas window and drag it to any environment (or click on NOT FALSE).
  • There is also an alternate form of the FALSE law that is triggered when one clicks or drags on the FALSE formula rather than the NOT FALSE formula.
  • Another feature that can be of some minor convenience: if a formula already exists in an enviroment, you can create a copy in the Formulas window by dragging to that window.
  1. Deduce A [assuming A]. [IMPLICATION INTRODUCTION]
  2. Deduce TRUE [assuming A]. [TRUE]
  3. From TRUE [assuming A], A [assuming A]: deduce TRUE AND A [assuming A]. [CONJUNCTION INTRODUCTION]
  4. Deduce TRUE AND A [assuming TRUE AND A]. [IMPLICATION INTRODUCTION]
  5. From TRUE AND A [assuming TRUE AND A]: deduce A [assuming TRUE AND A]. [CONJUNCTION ELIMINATION (right)]
  6. From A [assuming TRUE AND A], TRUE AND A [assuming A]: deduce A IFF (TRUE AND A). [BICONDITIONAL INTRODUCTION (ASSUMPTION FORM)]
  7. QED!
FALSE IS IDENTITY FOR OR
  1. Deduce A [assuming A]. [IMPLICATION INTRODUCTION]
  2. From A [assuming A]: deduce FALSE OR A [assuming A]. [DISJUNCTION INTRODUCTION (right)]
  3. Deduce FALSE OR A [assuming FALSE OR A]. [IMPLICATION INTRODUCTION]
  4. Deduce NOT FALSE [assuming FALSE OR A]. [NOT FALSE]
  5. From FALSE OR A [assuming FALSE OR A], NOT FALSE [assuming FALSE OR A]: deduce A [assuming FALSE OR A]. [DISJUNCTIVE ELIMINATION (left)]
  6. From A [assuming FALSE OR A], FALSE OR A [assuming A]: deduce A IFF (FALSE OR A). [BICONDITIONAL INTRODUCTION (ASSUMPTION FORM)]
  7. QED!
FALSE ANNULS AND
Thanks to Pace Nielsen, Elliot Parlin, Adam Glasgall, Ephim Kolmogorov, and Loren Spice for a short proof.
  1. Deduce NOT FALSE. [NOT FALSE]
  2. From NOT FALSE: deduce (NOT FALSE) OR (NOT A). [DISJUNCTION INTRODUCTION (left)]
  3. From (NOT FALSE) OR (NOT A): deduce NOT (FALSE AND A). [DE MORGAN'S LAW II]
  4. QED!
TRUE ANNULS OR
  1. Deduce TRUE. [TRUE]
  2. From TRUE: deduce TRUE OR A. [DISJUNCTION INTRODUCTION (left)]
  3. QED!
EX FALSO QUODLIBET (boolean version)
Thanks to Anders Kaseorg, Jacob Hobbs, and Pace Nielsen for the short proof.
  1. Deduce NOT FALSE. [NOT FALSE]
  2. From NOT FALSE: deduce (NOT FALSE) OR A. [DISJUNCTION INTRODUCTION (left)]
  3. From (NOT FALSE) OR A: deduce FALSE IMPLIES A. [EXERCISE 12.4(b)]
  4. QED!
  1. Deduce A [assuming A]. [IMPLICATION INTRODUCTION]
  2. Deduce TRUE [assuming A]. [TRUE]
  3. From TRUE [assuming A]: deduce A IMPLIES TRUE. [DEDUCTION THEOREM]
  4. QED!
  1. Deduce A IMPLIES (TRUE IMPLIES A). [EXERCISE 7.1]
  2. Deduce TRUE IMPLIES A [assuming TRUE IMPLIES A]. [IMPLICATION INTRODUCTION]
  3. Deduce TRUE [assuming TRUE IMPLIES A]. [TRUE]
  4. From TRUE [assuming TRUE IMPLIES A], TRUE IMPLIES A [assuming TRUE IMPLIES A]: deduce A [assuming TRUE IMPLIES A]. [MODUS PONENS]
  5. From A [assuming TRUE IMPLIES A]: deduce (TRUE IMPLIES A) IMPLIES A. [DEDUCTION THEOREM]
  6. From A IMPLIES (TRUE IMPLIES A), (TRUE IMPLIES A) IMPLIES A: deduce A IFF (TRUE IMPLIES A). [BICONDITIONAL INTRODUCTION]
  7. QED!
Thanks to Anders Kaseorg for the short proof, to Jacob Hobbs for a shorter proof, and to Pace Nielsen for an even shorter proof.
  1. Deduce A IMPLIES FALSE [assuming A IMPLIES FALSE]. [IMPLICATION INTRODUCTION]
  2. Deduce NOT FALSE [assuming A IMPLIES FALSE]. [NOT FALSE]
  3. From A IMPLIES FALSE [assuming A IMPLIES FALSE], NOT FALSE [assuming A IMPLIES FALSE]: deduce NOT A [assuming A IMPLIES FALSE]. [MODUS TOLLENS]
  4. Deduce NOT A [assuming NOT A]. [IMPLICATION INTRODUCTION]
  5. From NOT A [assuming NOT A]: deduce (NOT A) OR FALSE [assuming NOT A]. [DISJUNCTION INTRODUCTION (left)]
  6. From (NOT A) OR FALSE [assuming NOT A]: deduce A IMPLIES FALSE [assuming NOT A]. [EXERCISE 12.4(b)]
  7. From NOT A [assuming A IMPLIES FALSE], A IMPLIES FALSE [assuming NOT A]: deduce (NOT A) IFF (A IMPLIES FALSE). [BICONDITIONAL INTRODUCTION (ASSUMPTION FORM)]
  8. QED!
  • In previous sections we were working in the simple setting of propositional logic, in which the atomic propositions were given short names such as A, B, or C, and had no further internal structure. We now begin the exploration of a powerful extension of this logic known as first-order logic (or predicate logic), in which the atomic propositions may now depend on one or more variables such as x, y, z. First-order logic is the standard logical framework for most of modern mathematics.
  • For now, we focus on the type of variable known as free variables.
  • A free variable can take any value within a given domain of discourse. The precise domain of discourse used is important when applying first-order logic to mathematical situations; for instance, if one is doing number theory, the domain of discourse might be the real numbers, while if one is doing group theory, domain of discourse might be the collection of elements of the group. For more complicated mathematics, the domain of discourse may be the universe of sets. However the rules of first-order logic do not care exactly what this domain is, so we will usually leave the domain unspecified.
  • In previous sections, we created sub-environments of the Root environment in which certain sentences were assumed to be true. In first-order logic, one can also create sub-environments in which new free variables are introduced and allowed to range freely in the domain of discourse. Any statement in such a sub-environment is known to be true for all values of this variable.
  • All the usual laws of propositional logic apply within such sub-environments, with one new wrinkle: if one wants to use a sentence such as P(x) that depends on a variable x, one can only do so inside an environment in which that variable has been introduced. For instance, P(x) cannot be directly used in the Root environment, but can be used in a sub-environment where x is arbitrary. (Try dragging P(x) or Q(x) to various environments to see what happens!)
  • Technical note: matching for this exercise has not yet been implemented (thus, this exercise will not appear in subsequent available deductions). I hope to implement this functionality in the future. Many further exercises will also have matching not implemented.
  • Thanks to Martin Epstein for a short proof.
  1. P(x) [letting x be arbitrary]. [given]
  2. Deduce P(x) IMPLIES (Q(x) IMPLIES P(x)) [letting x be arbitrary]. [EXERCISE 7.1]
  3. From P(x) [letting x be arbitrary], P(x) IMPLIES (Q(x) IMPLIES P(x)) [letting x be arbitrary]: deduce Q(x) IMPLIES P(x) [letting x be arbitrary]. [MODUS PONENS]
  4. From Q(x) IMPLIES P(x) [letting x be arbitrary]: deduce Q(x) IMPLIES (P(x) AND Q(x)) [letting x be arbitrary]. [ABSORPTION (left)]
  5. QED! (again)
  • We already know that a sentence (such as A) can be pushed into a sub-environment in which an additional statement (such as B) is assumed.
  • Similarly, we may push a sentence into a sub-environment in which an additional free variable (such as x) is introduced.
  • By invoking the push law in this fashion, we may end up with statements that do not depend on all of the ambient free variables, but this is perfectly acceptable in first-order logic. (However, as mentioned previously, in any given environment, it is not permitted to work with sentences that depend on free variables that have not been introduced into that environment.)
  • Technical note: matching for this exercise has not yet been implemented.
  1. P(x) [letting x be arbitrary]. [given]
  2. Q(x, y) [letting x, y be arbitrary]. [given]
  3. From P(x) [letting x be arbitrary]: deduce P(x) [letting x, y be arbitrary]. [PUSH (for free variables)]
  4. From P(x) [letting x, y be arbitrary], Q(x, y) [letting x, y be arbitrary]: deduce P(x) AND Q(x, y) [letting x, y be arbitrary]. [CONJUNCTION INTRODUCTION]
  5. QED!
DOUBLE PUSH (for free variables)
This is the analogue of the DOUBLE PUSH law for assumptions introduced in Exercise 7.2, and can similarly be used to shorten some of the proofs in subsequent exercises.
  1. A. [given]
  2. Form environment [letting x, y be arbitrary]. [given]
  3. From A: deduce A [letting x be arbitrary]. [PUSH (for free variables)]
  4. From A [letting x be arbitrary]: deduce A [letting x, y be arbitrary]. [PUSH (for free variables)]
  5. QED!
DOUBLE PUSH (mixed version I)
It will also be helpful to have "mixed" double pushes involving both assumptions and arbitrary variables.
  1. A. [given]
  2. Form environment [assuming B, letting x be arbitrary]. [given]
  3. From A: deduce A [assuming B]. [PUSH]
  4. From A [assuming B]: deduce A [assuming B, letting x be arbitrary]. [PUSH (for free variables)]
  5. QED!
DOUBLE PUSH (mixed version II)
  1. A. [given]
  2. Form environment [letting x be arbitrary, assuming B]. [given]
  3. From A: deduce A [letting x be arbitrary]. [PUSH (for free variables)]
  4. From A [letting x be arbitrary]: deduce A [letting x be arbitrary, assuming B]. [PUSH]
  5. QED!
  • In any environment, one may introduce any free variable that is not already in use, thus forming a new environment in which that free variable is arbitrary.
  • To do this, drag a free variable from the (now unlocked) Terms window to the target environment (or, if one wants to start from the root environment, one can just click on a free variable).
  • If all the free variables in the Terms window are already in use, you can click on the "New free variable" button to create a further free variable.
  • Later, we will introduce some other types of terms than free variables, namely bound variables, primitive terms, and operators applied to other terms. But for now, the Terms window will only be occupied by free variables.
  • Technical note: matching for this exercise has not yet been implemented.
  1. Form environment [letting x be arbitrary]. [FREE VARIABLE INTRODUCTION]
  2. Form environment [letting x, y be arbitrary]. [FREE VARIABLE INTRODUCTION]
  3. Deduce Q(x, y) OR (NOT Q(x, y)) [letting x, y be arbitrary]. [EXCLUDED MIDDLE]
  4. QED!
  • Recall the deduction theorem, which allowed one to convert a statement A that was only known conditionally on an assumption B, to a statement A IMPLIES B that was known unconditionally.
  • In a similar spirit, we have the law of universal introduction: if one has established a statement P(x) under the assumption that the free variable x be arbitrary, then one can conclude the statement FOR ALL X: P(X) unconditionally.
  • Note that it is the immediate environment of the statement P(x) that has to be of the form "Let x be arbitrary"; the law of universal quantification is not available if P(x) is deeply nested inside such an environment.
  • Here X is a different type of variable than a free variable, namely a bound variable. P(X) is formed from P(x) by replacing every occurrence of the free variable x in P(x) with the bound variable X.
  • Bound variables need to have different names from free variables; in this text, we ensure this by using lower case letters such as x, y, z for free variables and upper case variables such as X, Y, Z for bound variables. (Note: this convention is not standard in the mathematics literature; usually, one sees free and bound variables share the same namespace, and then one has to ensure that a variable is not simultaneously used as a free variable and as a bound variable.)
  • Both free and bound variables will be placed in the Terms window. In later sections we will also introduce further types of terms.
  • A bound variable such as X can only be used in statements in various environments if they are "bound" by an appropriate quantifier.
  • For instance, the formula P(X) cannot be directly used in environment windows right now, as it is not bound by a quantifier. (However, we still consider it to be a valid formula.)
  • Currently, the only available quantifier is the universal quantifier "FOR ALL"; later we will also introduce the existential quantifier "THERE EXISTS".
  • Quantifiers can be nested, as long as each quantifier uses different bound variables: "FOR ALL X: (FOR ALL Y: Q(X,Y))" is a valid formula, but "FOR ALL X: (FOR ALL X: Q(X,X))" is not.
  • To use the law of universal introduction, either drag a statement (in which some free variable is arbitrary) to a bound variable in the Terms window, or drag it to the parent environment.
  • In the former case, the bound variable selected will be used to perform universal quantification. In the latter case, the text will pick the next available bound variable.
  • As with free variables, a button is now provided to produce additional bound variables, should this prove necessary.
  • Technical note: matching for this exercise has not yet been implemented.
  1. Form environment [letting x be arbitrary]. [FREE VARIABLE INTRODUCTION]
  2. Deduce P(x) IMPLIES P(x) [letting x be arbitrary]. [IMPLIES IS IDEMPOTENT]
  3. From P(x) IMPLIES P(x) [letting x be arbitrary]: deduce FOR ALL X: (P(X) IMPLIES P(X)). [UNIVERSAL INTRODUCTION]
  4. QED!
  • To create a formula of the form "FOR ALL X: P(X)", create the formula "P(X)" and drag it to the bound variable X (or vice versa).
  • As previously noted, we allow the Formulas window to contain formulas such as Q(X,Y) that contain unquantified bound variables. As such, these formulas cannot be directly used in an environment window; however, after enclosing such formulas in quantifiers to bound all the bound variables, it becomes legal to use them in those windows.
  • Technical note: matching for this exercise has not yet been implemented.
  1. Deduce (FOR ALL X: (FOR ALL Y: Q(X, Y))) IMPLIES (FOR ALL X: (FOR ALL Y: Q(X, Y))). [IMPLIES IS IDEMPOTENT]
  2. QED!
  • There is a reverse to the law of universal introduction, known as the law of universal specification. It asserts that if FOR ALL X: P(X) is true, and α is a term which is well-defined in the sense that it does not involve bound variables or free variables not present in the environment, then P(α) is also true.
  • Here, X is a bound variable, P(X) is any statement that can involve the variable X.
  • At present, the only terms you have seen are free variables and bound variables, so the law can only be currently applied to free variables α. However, some further examples of terms will be introduced later.
  • As with all other laws, this law is only applicable if the conclusion P(α) is well-formed: in particular, the statement P(α) cannot use free variables that are not present in the environment, nor can it have nested quantifiers involving the same bound variable.
  • The law of universal specification can fail if one permits α to contain bound variables. For instance, using the natural numbers as the domain of discourse, the sentence "FOR ALL X: THERE EXISTS Y: Y=X+1" is true (every natural number has a successor), but one cannot specify X to equal Y to conclude the (incorrect) statement THERE EXISTS Y: Y=Y+1. However, if y is an ambient free variable in the current environment, one may specify X to equal y and conclude THERE EXISTS Y: Y=y+1.
  • To use the law of universal specification, drag a sentence of the form FOR ALL X: P(X) to a term α or vice versa.
  • Note that currently the law does not work in the Root environment, because the unquantified bound variables X,Y cannot be used in this environment; similarly for any further free and bound variables one creates. How would one get around this problem?
  • The presence of the term Y in the hypotheses has no impact on how this exercise is proven, but affects how the exercise can be used in subsequent problems. Namely, to invoke this exercise, drag a sentence of the form FOR ALL X: P(X) to a term of the form Y (or vice versa).
  1. FOR ALL X: P(X). [given]
  2. Form environment [letting x be arbitrary]. [FREE VARIABLE INTRODUCTION]
  3. From FOR ALL X: P(X): deduce FOR ALL X: P(X) [letting x be arbitrary]. [PUSH (for free variables)]
  4. From FOR ALL X: P(X) [letting x be arbitrary]: deduce P(x) [letting x be arbitrary]. [UNIVERSAL SPECIFICATION]
  5. From P(x) [letting x be arbitrary]: deduce FOR ALL Y: P(Y). [ UNIVERSAL INTRODUCTION]
  6. QED!
  1. A. [given]
  2. Form environment [letting x be arbitrary]. [FREE VARIABLE INTRODUCTION]
  3. From A: deduce A [letting x be arbitrary]. [PUSH (for free variables)]
  4. From A [letting x be arbitrary]: deduce FOR ALL X: A. [ UNIVERSAL INTRODUCTION]
  5. QED!
  • This exercise, which reverses the universal introduction law from Section 17, will be helpful in some later exercises. (As such, matching has been implemented for this exercise.)
  • To use it, drag a statement of the form FOR ALL X: P(X) onto a free variable term such as x (or vice versa).
  1. FOR ALL X: P(X). [given]
  2. Form environment [letting x be arbitrary]. [FREE VARIABLE INTRODUCTION]
  3. From FOR ALL X: P(X): deduce FOR ALL X: P(X) [letting x be arbitrary]. [PUSH (for free variables)]
  4. From FOR ALL X: P(X) [letting x be arbitrary]: deduce P(x) [letting x be arbitrary]. [UNIVERSAL SPECIFICATION]
  5. QED!
  • The classical syllogisms of Aristotelian logic consisted of two premises (a major premise and a minor premise), and a conclusion that could be drawn from those premises. These syllogisms can be interpreted using the more modern language of first-order logic.
  • One of the classical syllogisms is the Barbara syllogism. A famous example of this syllogism (in its singular form) is "All men are mortal. Socrates is a man. Hence, Socrates is mortal."
  • In this exercise, we model this syllogism by using P(X) to denote the statement "X is a man", Q(X) to denote the statement "X is a mortal", and α to denote Socrates.
  • The term α is an example of a primitive term - neither a free variable or a bound variable, but an object or quantity that one can use in one's arguments.
  • Primitive terms are to terms as atomic propositions such as A, B, C are to propositions. To avoid confusion with other objects in first-order logic, we will use Greek letters such as α, β, γ to refer to primitive terms (or more generally to terms that are not required to be free or bound variables).
  • Most of the other classical syllogisms will be treated in Section 22.
  • The presence of the term α in the hypotheses is not needed to solve the exercise, but affects how the exercise is invoked in subsequent applications. Namely, to apply this exercise, one drags a sentence of the form FOR ALL X: P(X) IMPLIES Q(X) to a sentence of the form P(α), and then CTRL-clicks on the term α.
  1. FOR ALL X: (P(X) IMPLIES Q(X)). [given]
  2. P(α). [given]
  3. From FOR ALL X: (P(X) IMPLIES Q(X)): deduce P(α) IMPLIES Q(α). [UNIVERSAL SPECIFICATION]
  4. From P(α), P(α) IMPLIES Q(α): deduce Q(α). [MODUS PONENS]
  5. QED!
BARBARA SYLLOGISM (classical form)
  • There is another, more classical, form of the Barbara syllogism, a typical example of which is "All men are mortal. All Greeks are men. Hence, all Greeks are mortal".
  • Again, we can model this in first-order logic as before, where now R(X) denotes the statement "X is Greek".
  • We will present the other classical syllogisms of Aristotelian logic later in this text.
  1. FOR ALL X: (P(X) IMPLIES Q(X)). [given]
  2. FOR ALL X: (R(X) IMPLIES P(X)). [given]
  3. From FOR ALL X: (P(X) IMPLIES Q(X)): deduce P(x) IMPLIES Q(x) [letting x be arbitrary]. [REVERSE UNIVERSAL INTRODUCTION]
  4. From FOR ALL X: (R(X) IMPLIES P(X)): deduce R(x) IMPLIES P(x) [letting x be arbitrary]. [REVERSE UNIVERSAL INTRODUCTION]
  5. From R(x) IMPLIES P(x) [letting x be arbitrary], P(x) IMPLIES Q(x) [letting x be arbitrary]: deduce R(x) IMPLIES Q(x) [letting x be arbitrary]. [IMPLIES IS TRANSITIVE]
  6. From R(x) IMPLIES Q(x) [letting x be arbitrary]: deduce FOR ALL X: (R(X) IMPLIES Q(X)). [ UNIVERSAL INTRODUCTION]
  7. QED!
FOR ALL IS COMMUTATIVE
  • Thanks to Anders Kaseorg for the short proof.
  1. FOR ALL X: (FOR ALL Y: Q(X, Y)). [given]
  2. Form environment [letting y be arbitrary]. [FREE VARIABLE INTRODUCTION]
  3. From FOR ALL X: (FOR ALL Y: Q(X, Y)): deduce FOR ALL X: (FOR ALL Y: Q(X, Y)) [letting y be arbitrary]. [PUSH (for free variables)]
  4. From FOR ALL X: (FOR ALL Y: Q(X, Y)) [letting y be arbitrary]: deduce FOR ALL Y: Q(x, Y) [letting y, x be arbitrary]. [REVERSE UNIVERSAL INTRODUCTION]
  5. From FOR ALL Y: Q(x, Y) [letting y, x be arbitrary]: deduce Q(x, y) [letting y, x be arbitrary]. [UNIVERSAL SPECIFICATION]
  6. From Q(x, y) [letting y, x be arbitrary]: deduce FOR ALL X: Q(X, y) [letting y be arbitrary]. [ UNIVERSAL INTRODUCTION]
  7. From FOR ALL X: Q(X, y) [letting y be arbitrary]: deduce FOR ALL Y: (FOR ALL X: Q(X, Y)). [ UNIVERSAL INTRODUCTION]
  8. QED!
AND DISTRIBUTES OVER FOR ALL
  • Thanks to Elliot Parlin, Keith Winstein, and Andrew Lei for a (relatively) short proof (which has since been shortened further using some additional helper exercises.)
  1. Deduce FOR ALL X: (P(X) AND Q(X)) [assuming FOR ALL X: (P(X) AND Q(X))]. [IMPLICATION INTRODUCTION]
  2. From FOR ALL X: (P(X) AND Q(X)) [assuming FOR ALL X: (P(X) AND Q(X))]: deduce P(x) AND Q(x) [assuming FOR ALL X: (P(X) AND Q(X)), letting x be arbitrary]. [REVERSE UNIVERSAL INTRODUCTION]
  3. From P(x) AND Q(x) [assuming FOR ALL X: (P(X) AND Q(X)), letting x be arbitrary]: deduce P(x) [assuming FOR ALL X: (P(X) AND Q(X)), letting x be arbitrary]. [CONJUNCTION ELIMINATION (left)]
  4. From P(x) AND Q(x) [assuming FOR ALL X: (P(X) AND Q(X)), letting x be arbitrary]: deduce Q(x) [assuming FOR ALL X: (P(X) AND Q(X)), letting x be arbitrary]. [CONJUNCTION ELIMINATION (right)]
  5. From P(x) [assuming FOR ALL X: (P(X) AND Q(X)), letting x be arbitrary]: deduce FOR ALL X: P(X) [assuming FOR ALL X: (P(X) AND Q(X))]. [ UNIVERSAL INTRODUCTION]
  6. From Q(x) [assuming FOR ALL X: (P(X) AND Q(X)), letting x be arbitrary]: deduce FOR ALL X: Q(X) [assuming FOR ALL X: (P(X) AND Q(X))]. [ UNIVERSAL INTRODUCTION]
  7. From FOR ALL X: P(X) [assuming FOR ALL X: (P(X) AND Q(X))], FOR ALL X: Q(X) [assuming FOR ALL X: (P(X) AND Q(X))]: deduce (FOR ALL X: P(X)) AND (FOR ALL X: Q(X)) [assuming FOR ALL X: (P(X) AND Q(X))]. [CONJUNCTION INTRODUCTION]
  8. Deduce (FOR ALL X: P(X)) AND (FOR ALL X: Q(X)) [assuming (FOR ALL X: P(X)) AND (FOR ALL X: Q(X))]. [IMPLICATION INTRODUCTION]
  9. From (FOR ALL X: P(X)) AND (FOR ALL X: Q(X)) [assuming (FOR ALL X: P(X)) AND (FOR ALL X: Q(X))]: deduce FOR ALL X: P(X) [assuming (FOR ALL X: P(X)) AND (FOR ALL X: Q(X))]. [CONJUNCTION ELIMINATION (left)]
  10. From (FOR ALL X: P(X)) AND (FOR ALL X: Q(X)) [assuming (FOR ALL X: P(X)) AND (FOR ALL X: Q(X))]: deduce FOR ALL X: Q(X) [assuming (FOR ALL X: P(X)) AND (FOR ALL X: Q(X))]. [CONJUNCTION ELIMINATION (right)]
  11. From FOR ALL X: P(X) [assuming (FOR ALL X: P(X)) AND (FOR ALL X: Q(X))]: deduce P(x) [assuming (FOR ALL X: P(X)) AND (FOR ALL X: Q(X)), letting x be arbitrary]. [REVERSE UNIVERSAL INTRODUCTION]
  12. From FOR ALL X: Q(X) [assuming (FOR ALL X: P(X)) AND (FOR ALL X: Q(X))]: deduce Q(x) [assuming (FOR ALL X: P(X)) AND (FOR ALL X: Q(X)), letting x be arbitrary]. [REVERSE UNIVERSAL INTRODUCTION]
  13. From P(x) [assuming (FOR ALL X: P(X)) AND (FOR ALL X: Q(X)), letting x be arbitrary], Q(x) [assuming (FOR ALL X: P(X)) AND (FOR ALL X: Q(X)), letting x be arbitrary]: deduce P(x) AND Q(x) [assuming (FOR ALL X: P(X)) AND (FOR ALL X: Q(X)), letting x be arbitrary]. [CONJUNCTION INTRODUCTION]
  14. From P(x) AND Q(x) [assuming (FOR ALL X: P(X)) AND (FOR ALL X: Q(X)), letting x be arbitrary]: deduce FOR ALL X: (P(X) AND Q(X)) [assuming (FOR ALL X: P(X)) AND (FOR ALL X: Q(X))]. [ UNIVERSAL INTRODUCTION]
  15. From FOR ALL X: (P(X) AND Q(X)) [assuming (FOR ALL X: P(X)) AND (FOR ALL X: Q(X))], (FOR ALL X: P(X)) AND (FOR ALL X: Q(X)) [assuming FOR ALL X: (P(X) AND Q(X))]: deduce (FOR ALL X: (P(X) AND Q(X))) IFF ((FOR ALL X: P(X)) AND (FOR ALL X: Q(X))). [BICONDITIONAL INTRODUCTION (ASSUMPTION FORM)]
  16. QED!
IMPLIES COMMUTES WITH FOR ALL
  • Thanks to Gesse Roure for a short proof.
  1. Deduce A IMPLIES (FOR ALL X: P(X)) [assuming A IMPLIES (FOR ALL X: P(X))]. [IMPLICATION INTRODUCTION]
  2. Form environment [assuming A IMPLIES (FOR ALL X: P(X)), letting x be arbitrary]. [FREE VARIABLE INTRODUCTION]
  3. From A IMPLIES (FOR ALL X: P(X)) [assuming A IMPLIES (FOR ALL X: P(X))]: deduce A IMPLIES (FOR ALL X: P(X)) [assuming A IMPLIES (FOR ALL X: P(X)), letting x be arbitrary]. [PUSH (for free variables)]
  4. From A IMPLIES (FOR ALL X: P(X)) [assuming A IMPLIES (FOR ALL X: P(X)), letting x be arbitrary]: deduce FOR ALL X: P(X) [assuming A IMPLIES (FOR ALL X: P(X)), letting x be arbitrary, assuming A]. [REVERSE DEDUCTION THEOREM]
  5. From FOR ALL X: P(X) [assuming A IMPLIES (FOR ALL X: P(X)), letting x be arbitrary, assuming A]: deduce P(x) [assuming A IMPLIES (FOR ALL X: P(X)), letting x be arbitrary, assuming A]. [UNIVERSAL SPECIFICATION]
  6. From P(x) [assuming A IMPLIES (FOR ALL X: P(X)), letting x be arbitrary, assuming A]: deduce A IMPLIES P(x) [assuming A IMPLIES (FOR ALL X: P(X)), letting x be arbitrary]. [DEDUCTION THEOREM]
  7. From A IMPLIES P(x) [assuming A IMPLIES (FOR ALL X: P(X)), letting x be arbitrary]: deduce FOR ALL X: (A IMPLIES P(X)) [assuming A IMPLIES (FOR ALL X: P(X))]. [ UNIVERSAL INTRODUCTION]
  8. Deduce FOR ALL X: (A IMPLIES P(X)) [assuming FOR ALL X: (A IMPLIES P(X))]. [IMPLICATION INTRODUCTION]
  9. Deduce A [assuming FOR ALL X: (A IMPLIES P(X)), A]. [IMPLICATION INTRODUCTION]
  10. From FOR ALL X: (A IMPLIES P(X)) [assuming FOR ALL X: (A IMPLIES P(X))]: deduce FOR ALL X: (A IMPLIES P(X)) [assuming FOR ALL X: (A IMPLIES P(X)), A]. [PUSH]
  11. From FOR ALL X: (A IMPLIES P(X)) [assuming FOR ALL X: (A IMPLIES P(X)), A]: deduce A IMPLIES P(x) [assuming FOR ALL X: (A IMPLIES P(X)), A, letting x be arbitrary]. [REVERSE UNIVERSAL INTRODUCTION]
  12. From A [assuming FOR ALL X: (A IMPLIES P(X)), A]: deduce A [assuming FOR ALL X: (A IMPLIES P(X)), A, letting x be arbitrary]. [PUSH (for free variables)]
  13. From A [assuming FOR ALL X: (A IMPLIES P(X)), A, letting x be arbitrary], A IMPLIES P(x) [assuming FOR ALL X: (A IMPLIES P(X)), A, letting x be arbitrary]: deduce P(x) [assuming FOR ALL X: (A IMPLIES P(X)), A, letting x be arbitrary]. [MODUS PONENS]
  14. From P(x) [assuming FOR ALL X: (A IMPLIES P(X)), A, letting x be arbitrary]: deduce FOR ALL X: P(X) [assuming FOR ALL X: (A IMPLIES P(X)), A]. [ UNIVERSAL INTRODUCTION]
  15. From FOR ALL X: P(X) [assuming FOR ALL X: (A IMPLIES P(X)), A]: deduce A IMPLIES (FOR ALL X: P(X)) [assuming FOR ALL X: (A IMPLIES P(X))]. [DEDUCTION THEOREM]
  16. From A IMPLIES (FOR ALL X: P(X)) [assuming FOR ALL X: (A IMPLIES P(X))], FOR ALL X: (A IMPLIES P(X)) [assuming A IMPLIES (FOR ALL X: P(X))]: deduce (A IMPLIES (FOR ALL X: P(X))) IFF (FOR ALL X: (A IMPLIES P(X))). [BICONDITIONAL INTRODUCTION (ASSUMPTION FORM)]
  17. QED!
  • There is a twin sibling to the universal quantifier FOR ALL, namely the existential quantifier THERE EXISTS. As the name suggests, the sentence THERE EXISTS X: P(X) should be interpreted as the assertion that there exists a choice of X in the domain of discourse such that P(X) is true.
  • One can formalise this using the law of existential instantiation. This law asserts that if THERE EXISTS X: P(X) is true, and x is an available free variable, then one can set x to a value for which P(x) holds.
  • In this text, this is depicted by a subenvironment entitled Set x s.t. P(x). This is an environment similar to an environment introducing a free variable, but now the variable x is not free to range throughout the domain of discourse, but instead has to obey P(x).
  • The PUSH law extends to these environments also, by the usual mechanism of dragging a statement into the environment where x is set.
  • To use the existential instantiation law, drag a statement of the form THERE EXISTS X: P(X) to a free variable. One can also simply click on the law, and the text will try to locate an available free variable to use.
  • Technical note: matching for this exercise has not yet been implemented.
  1. THERE EXISTS X: P(X). [given]
  2. FOR ALL X: Q(X). [given]
  3. From THERE EXISTS X: P(X): deduce P(x) [setting x s.t. P(x)]. [EXISTENTIAL INSTANTIATION]
  4. From FOR ALL X: Q(X): deduce FOR ALL X: Q(X) [setting x s.t. P(x)]. [PUSH (for set variables)]
  5. From FOR ALL X: Q(X) [setting x s.t. P(x)]: deduce Q(x) [setting x s.t. P(x)]. [UNIVERSAL SPECIFICATION]
  6. From P(x) [setting x s.t. P(x)], Q(x) [setting x s.t. P(x)]: deduce P(x) AND Q(x) [setting x s.t. P(x)]. [CONJUNCTION INTRODUCTION]
  7. QED!
DOUBLE PUSH (mixed III)
  1. A. [given]
  2. Form environment [assuming B, setting x s.t. C]. [given]
  3. From A: deduce A [assuming B]. [PUSH]
  4. From A [assuming B]: deduce A [assuming B, setting x s.t. C]. [PUSH (for set variables)]
  5. QED!
DOUBLE PUSH (mixed IV)
  1. A. [given]
  2. Form environment [setting x s.t. C, assuming B]. [given]
  3. From A: deduce A [setting x s.t. C]. [PUSH (for set variables)]
  4. From A [setting x s.t. C]: deduce A [setting x s.t. C, assuming B]. [PUSH]
  5. QED!
DOUBLE PUSH (mixed V)
  1. A. [given]
  2. Form environment [setting x s.t. C, letting y be arbitrary]. [given]
  3. From A: deduce A [setting x s.t. C]. [PUSH (for set variables)]
  4. From A [setting x s.t. C]: deduce A [setting x s.t. C, letting y be arbitrary]. [PUSH (for free variables)]
  5. QED!
DOUBLE PUSH (mixed VI)
  1. A. [given]
  2. Form environment [letting y be arbitrary, setting x s.t. C]. [given]
  3. From A: deduce A [letting y be arbitrary]. [PUSH (for free variables)]
  4. From A [letting y be arbitrary]: deduce A [letting y be arbitrary, setting x s.t. C]. [PUSH (for set variables)]
  5. QED!
DOUBLE PUSH (for set variables)
  1. A. [given]
  2. Form environment [setting y s.t. B, setting x s.t. C]. [given]
  3. From A: deduce A [setting y s.t. B]. [PUSH (for set variables)]
  4. From A [setting y s.t. B]: deduce A [setting y s.t. B, setting x s.t. C]. [PUSH (for set variables)]
  5. QED!
PULL (existential form)
  • There is a reverse to the PUSH law (for variables x that have been set to obey a certain property): if a statement A is known to hold for some set value of x, and the statement A does not involve the variable x, then one can pull A out of that environment and conclude that A holds unconditionally.
  • Of course, if A does depend on x, then no such pull is possible, since the statement A is not even well-formed once one leaves the environment where x is being set.
  • There are two ways to invoke the PULL law. Either drag a statement A in an environment where a variable x is set outside of that environment, or simply click on A.
  1. THERE EXISTS X: A. [given]
  2. From THERE EXISTS X: A: deduce A [setting x s.t. A]. [EXISTENTIAL INSTANTIATION]
  3. From A [setting x s.t. A]: deduce A. [PULL]
  4. QED!
DOUBLE PULL
  1. A [setting y s.t. C, setting x s.t. B]. [given]
  2. From A [setting y s.t. C, setting x s.t. B]: deduce A [setting y s.t. C]. [PULL]
  3. From A [setting y s.t. C]: deduce A. [PULL]
  4. QED!
PULL (for arbitrary variables)
  • Recall that all variables in first-order logic are understood to range in some domain of discourse. However, so far we have not precluded the possibility that this domain of discourse is empty, so that there are no possible values for such variables to take!
  • This is of course a rather degenerate situation, in particular all existential statements of the form "THERE EXISTS X: P(X)" would automatically be false. To exclude it, we introduce the law of existence: there exists a quantity X for which the statement TRUE holds.
  • This law may seem trivial or redundant, but it actually cannot be deduced from the other laws in this text, and must be stated explicitly. (If one deletes this law, one obtains instead the theory of free logic, in which the domain of discourse is permitted to be empty.)
  • The error of assuming the law of existence when the domain of discourse is not known to be non-empty is known as the existential fallacy.
  • To use the law of existence, drag the TRUE statement (or the formula TRUE) onto a bound variable (or vice versa).
  1. A [letting x be arbitrary]. [given]
  2. From A [letting x be arbitrary]: deduce FOR ALL X: A. [ UNIVERSAL INTRODUCTION]
  3. Deduce THERE EXISTS X: TRUE. [EXISTENCE]
  4. From THERE EXISTS X: TRUE: deduce TRUE [setting x s.t. TRUE]. [EXISTENTIAL INSTANTIATION]
  5. From FOR ALL X: A: deduce FOR ALL X: A [setting x s.t. TRUE]. [PUSH (for set variables)]
  6. From FOR ALL X: A [setting x s.t. TRUE]: deduce A [setting x s.t. TRUE]. [UNIVERSAL SPECIFICATION]
  7. From A [setting x s.t. TRUE]: deduce A. [PULL]
  8. QED!
  • The law of existential introduction asserts that if one knows a statement of the form P(α), where α is a term that does not involve any bound variables or any free variables not present in the ambient environment, then one can deduce THERE EXISTS X: P(X), where X is a bound variable not already occuring in P(α). This is the main way in which existential statements are proven.
  • To use this law (with X chosen to be the next available bound variable), drag the sentence P(α) onto the term α (or vice versa).
  • If one wants to specify the bound variable as well, drag the sentence P(α) onto the term α and then CTRL-click on the bound variable X (or one can click on P(α) and then CTRL-click on both α and X.
  • Important note: dragging P(α) onto a bound variable X will not trigger this law (because this does not specify what the term α is that one is using to introduce the existential quantifier).
  • Note that if the expression P(α) contains multiple copies of α, then there will be multiple options for P(X), as one is permitted to change zero, one or more of the α into a copy of X. This can lead to a rather large number of possible ways to use the law of existential introduction if the statement P(α) contains many copies of α!
  • Technical note: matching for this exercise has not yet been implemented.
  1. Q(α, α). [given]
  2. From Q(α, α): deduce Q(α, α) AND Q(α, α). [AND IS IDEMPOTENT]
  3. From Q(α, α) AND Q(α, α): deduce THERE EXISTS X: (Q(α, X) AND Q(X, α)). [EXISTENTIAL INTRODUCTION]
  4. QED!
FOR ALL IMPLIES THERE EXISTS
  • This exercise will require the use of the law of existence, or a consequence of that law such as the "pull" law for arbitrary variables.
  • Thanks to Anders Kaseorg for a short proof.
  1. FOR ALL X: P(X). [given]
  2. From FOR ALL X: P(X): deduce P(x) [letting x be arbitrary]. [REVERSE UNIVERSAL INTRODUCTION]
  3. From P(x) [letting x be arbitrary]: deduce THERE EXISTS X: P(X) [letting x be arbitrary]. [EXISTENTIAL INTRODUCTION]
  4. From THERE EXISTS X: P(X) [letting x be arbitrary]: deduce THERE EXISTS X: P(X). [PULL (for arbitrary variables)]
  5. QED!
DE MORGAN'S LAW FOR QUANTIFIERS I
  • The formula P(x) provided in the hypotheses will end up being useful during the proof. However, it can be ignored for the purposes of applying this exercise.
  1. Deduce NOT (THERE EXISTS X: P(X)) [assuming NOT (THERE EXISTS X: P(X))]. [IMPLICATION INTRODUCTION]
  2. Form environment [assuming NOT (THERE EXISTS X: P(X)), letting x be arbitrary]. [FREE VARIABLE INTRODUCTION]
  3. Deduce P(x) [assuming NOT (THERE EXISTS X: P(X)), letting x be arbitrary, assuming P(x)]. [IMPLICATION INTRODUCTION]
  4. From P(x) [assuming NOT (THERE EXISTS X: P(X)), letting x be arbitrary, assuming P(x)]: deduce THERE EXISTS X: P(X) [assuming NOT (THERE EXISTS X: P(X)), letting x be arbitrary, assuming P(x)]. [EXISTENTIAL INTRODUCTION]
  5. From NOT (THERE EXISTS X: P(X)) [assuming NOT (THERE EXISTS X: P(X))]: deduce NOT (THERE EXISTS X: P(X)) [assuming NOT (THERE EXISTS X: P(X)), letting x be arbitrary, assuming P(x)]. [DOUBLE PUSH (mixed version II)]
  6. From THERE EXISTS X: P(X) [assuming NOT (THERE EXISTS X: P(X)), letting x be arbitrary, assuming P(x)], NOT (THERE EXISTS X: P(X)) [assuming NOT (THERE EXISTS X: P(X)), letting x be arbitrary, assuming P(x)]: deduce NOT P(x) [assuming NOT (THERE EXISTS X: P(X)), letting x be arbitrary]. [REDUCTIO AD ABSURDUM (separated form)]
  7. From NOT P(x) [assuming NOT (THERE EXISTS X: P(X)), letting x be arbitrary]: deduce FOR ALL X: (NOT P(X)) [assuming NOT (THERE EXISTS X: P(X))]. [ UNIVERSAL INTRODUCTION]
  8. Deduce FOR ALL X: (NOT P(X)) [assuming FOR ALL X: (NOT P(X))]. [IMPLICATION INTRODUCTION]
  9. Deduce THERE EXISTS X: P(X) [assuming FOR ALL X: (NOT P(X)), THERE EXISTS X: P(X)]. [IMPLICATION INTRODUCTION]
  10. From THERE EXISTS X: P(X) [assuming FOR ALL X: (NOT P(X)), THERE EXISTS X: P(X)]: deduce P(x) [assuming FOR ALL X: (NOT P(X)), THERE EXISTS X: P(X), setting x s.t. P(x)]. [EXISTENTIAL INSTANTIATION]
  11. From FOR ALL X: (NOT P(X)) [assuming FOR ALL X: (NOT P(X))]: deduce FOR ALL X: (NOT P(X)) [assuming FOR ALL X: (NOT P(X)), THERE EXISTS X: P(X), setting x s.t. P(x)]. [DOUBLE PUSH (mixed III)]
  12. From FOR ALL X: (NOT P(X)) [assuming FOR ALL X: (NOT P(X)), THERE EXISTS X: P(X), setting x s.t. P(x)]: deduce NOT P(x) [assuming FOR ALL X: (NOT P(X)), THERE EXISTS X: P(X), setting x s.t. P(x)]. [UNIVERSAL SPECIFICATION]
  13. From P(x) [assuming FOR ALL X: (NOT P(X)), THERE EXISTS X: P(X), setting x s.t. P(x)], NOT P(x) [assuming FOR ALL X: (NOT P(X)), THERE EXISTS X: P(X), setting x s.t. P(x)]: deduce P(x) AND (NOT P(x)) [assuming FOR ALL X: (NOT P(X)), THERE EXISTS X: P(X), setting x s.t. P(x)]. [CONJUNCTION INTRODUCTION]
  14. From P(x) AND (NOT P(x)) [assuming FOR ALL X: (NOT P(X)), THERE EXISTS X: P(X), setting x s.t. P(x)]: deduce TRUE AND (NOT TRUE) [assuming FOR ALL X: (NOT P(X)), THERE EXISTS X: P(X), setting x s.t. P(x)]. [EX FALSO QUODLIBET]
  15. From TRUE AND (NOT TRUE) [assuming FOR ALL X: (NOT P(X)), THERE EXISTS X: P(X), setting x s.t. P(x)]: deduce TRUE AND (NOT TRUE) [assuming FOR ALL X: (NOT P(X)), THERE EXISTS X: P(X)]. [PULL]
  16. From TRUE AND (NOT TRUE) [assuming FOR ALL X: (NOT P(X)), THERE EXISTS X: P(X)]: deduce NOT (THERE EXISTS X: P(X)) [assuming FOR ALL X: (NOT P(X))]. [REDUCTIO AD ABSURDUM]
  17. From NOT (THERE EXISTS X: P(X)) [assuming FOR ALL X: (NOT P(X))], FOR ALL X: (NOT P(X)) [assuming NOT (THERE EXISTS X: P(X))]: deduce (NOT (THERE EXISTS X: P(X))) IFF (FOR ALL X: (NOT P(X))). [BICONDITIONAL INTRODUCTION (ASSUMPTION FORM)]
  18. QED!
DE MORGAN'S LAW FOR QUANTIFIERS II
  • This one is rather tough; you may have to think in terms of double negatives.
  • Again, the formula P(x) should be ignored when applying this exercise in subsequent problems.
  • Thanks to Anders Kaseorg for a short proof, and Gesse Roure for an even shorter proof.
  1. Deduce NOT (FOR ALL X: P(X)) [assuming NOT (FOR ALL X: P(X))]. [IMPLICATION INTRODUCTION]
  2. Deduce NOT (THERE EXISTS X: (NOT P(X))) [assuming NOT (FOR ALL X: P(X)), NOT (THERE EXISTS X: (NOT P(X)))]. [IMPLICATION INTRODUCTION]
  3. Deduce (NOT (THERE EXISTS X: (NOT P(X)))) IFF (FOR ALL X: (NOT (NOT P(X)))) [assuming NOT (FOR ALL X: P(X)), NOT (THERE EXISTS X: (NOT P(X)))]. [DE MORGAN'S LAW FOR QUANTIFIERS I]
  4. From NOT (THERE EXISTS X: (NOT P(X))) [assuming NOT (FOR ALL X: P(X)), NOT (THERE EXISTS X: (NOT P(X)))], (NOT (THERE EXISTS X: (NOT P(X)))) IFF (FOR ALL X: (NOT (NOT P(X)))) [assuming NOT (FOR ALL X: P(X)), NOT (THERE EXISTS X: (NOT P(X)))]: deduce FOR ALL X: (NOT (NOT P(X))) [assuming NOT (FOR ALL X: P(X)), NOT (THERE EXISTS X: (NOT P(X)))]. [SUBSTITUTION]
  5. From FOR ALL X: (NOT (NOT P(X))) [assuming NOT (FOR ALL X: P(X)), NOT (THERE EXISTS X: (NOT P(X)))]: deduce NOT (NOT P(x)) [assuming NOT (FOR ALL X: P(X)), NOT (THERE EXISTS X: (NOT P(X))), letting x be arbitrary]. [REVERSE UNIVERSAL INTRODUCTION]
  6. From NOT (NOT P(x)) [assuming NOT (FOR ALL X: P(X)), NOT (THERE EXISTS X: (NOT P(X))), letting x be arbitrary]: deduce P(x) [assuming NOT (FOR ALL X: P(X)), NOT (THERE EXISTS X: (NOT P(X))), letting x be arbitrary]. [DOUBLE NEGATION (right)]
  7. From P(x) [assuming NOT (FOR ALL X: P(X)), NOT (THERE EXISTS X: (NOT P(X))), letting x be arbitrary]: deduce FOR ALL X: P(X) [assuming NOT (FOR ALL X: P(X)), NOT (THERE EXISTS X: (NOT P(X)))]. [ UNIVERSAL INTRODUCTION]
  8. From NOT (FOR ALL X: P(X)) [assuming NOT (FOR ALL X: P(X))]: deduce NOT (FOR ALL X: P(X)) [assuming NOT (FOR ALL X: P(X)), NOT (THERE EXISTS X: (NOT P(X)))]. [PUSH]
  9. From FOR ALL X: P(X) [assuming NOT (FOR ALL X: P(X)), NOT (THERE EXISTS X: (NOT P(X)))], NOT (FOR ALL X: P(X)) [assuming NOT (FOR ALL X: P(X)), NOT (THERE EXISTS X: (NOT P(X)))]: deduce NOT (NOT (THERE EXISTS X: (NOT P(X)))) [assuming NOT (FOR ALL X: P(X))]. [REDUCTIO AD ABSURDUM (separated form)]
  10. From NOT (NOT (THERE EXISTS X: (NOT P(X)))) [assuming NOT (FOR ALL X: P(X))]: deduce THERE EXISTS X: (NOT P(X)) [assuming NOT (FOR ALL X: P(X))]. [DOUBLE NEGATION (right)]
  11. Deduce THERE EXISTS X: (NOT P(X)) [assuming THERE EXISTS X: (NOT P(X))]. [IMPLICATION INTRODUCTION]
  12. From THERE EXISTS X: (NOT P(X)) [assuming THERE EXISTS X: (NOT P(X))]: deduce NOT P(x) [assuming THERE EXISTS X: (NOT P(X)), setting x s.t. NOT P(x)]. [EXISTENTIAL INSTANTIATION]
  13. Deduce FOR ALL X: P(X) [assuming THERE EXISTS X: (NOT P(X)), setting x s.t. NOT P(x), assuming FOR ALL X: P(X)]. [IMPLICATION INTRODUCTION]
  14. From FOR ALL X: P(X) [assuming THERE EXISTS X: (NOT P(X)), setting x s.t. NOT P(x), assuming FOR ALL X: P(X)]: deduce P(x) [assuming THERE EXISTS X: (NOT P(X)), setting x s.t. NOT P(x), assuming FOR ALL X: P(X)]. [UNIVERSAL SPECIFICATION]
  15. From NOT P(x) [assuming THERE EXISTS X: (NOT P(X)), setting x s.t. NOT P(x)]: deduce NOT P(x) [assuming THERE EXISTS X: (NOT P(X)), setting x s.t. NOT P(x), assuming FOR ALL X: P(X)]. [PUSH]
  16. From P(x) [assuming THERE EXISTS X: (NOT P(X)), setting x s.t. NOT P(x), assuming FOR ALL X: P(X)], NOT P(x) [assuming THERE EXISTS X: (NOT P(X)), setting x s.t. NOT P(x), assuming FOR ALL X: P(X)]: deduce NOT (FOR ALL X: P(X)) [assuming THERE EXISTS X: (NOT P(X)), setting x s.t. NOT P(x)]. [REDUCTIO AD ABSURDUM (separated form)]
  17. From NOT (FOR ALL X: P(X)) [assuming THERE EXISTS X: (NOT P(X)), setting x s.t. NOT P(x)]: deduce NOT (FOR ALL X: P(X)) [assuming THERE EXISTS X: (NOT P(X))]. [PULL]
  18. From NOT (FOR ALL X: P(X)) [assuming THERE EXISTS X: (NOT P(X))], THERE EXISTS X: (NOT P(X)) [assuming NOT (FOR ALL X: P(X))]: deduce (NOT (FOR ALL X: P(X))) IFF (THERE EXISTS X: (NOT P(X))). [BICONDITIONAL INTRODUCTION (ASSUMPTION FORM)]
  19. QED! (again)
CELARENT SYLLOGISM
  • An example of the Celarent syllogism is "No reptiles have fur. All snakes are reptiles. Hence, no snakes have fur."
  • Thanks to Anders Kaseorg for a short proof.
  • For the purposes of matching, the formulae P(x), Q(x), R(x) should be ignored.
  1. NOT (THERE EXISTS X: (P(X) AND Q(X))). [given]
  2. FOR ALL X: (R(X) IMPLIES P(X)). [given]
  3. Deduce THERE EXISTS X: (R(X) AND Q(X)) [assuming THERE EXISTS X: (R(X) AND Q(X))]. [IMPLICATION INTRODUCTION]
  4. From THERE EXISTS X: (R(X) AND Q(X)) [assuming THERE EXISTS X: (R(X) AND Q(X))]: deduce R(x) AND Q(x) [assuming THERE EXISTS X: (R(X) AND Q(X)), setting x s.t. R(x) AND Q(x)]. [EXISTENTIAL INSTANTIATION]
  5. From FOR ALL X: (R(X) IMPLIES P(X)): deduce FOR ALL X: (R(X) IMPLIES P(X)) [assuming THERE EXISTS X: (R(X) AND Q(X)), setting x s.t. R(x) AND Q(x)]. [DOUBLE PUSH (mixed III)]
  6. From FOR ALL X: (R(X) IMPLIES P(X)) [assuming THERE EXISTS X: (R(X) AND Q(X)), setting x s.t. R(x) AND Q(x)]: deduce R(x) IMPLIES P(x) [assuming THERE EXISTS X: (R(X) AND Q(X)), setting x s.t. R(x) AND Q(x)]. [UNIVERSAL SPECIFICATION]
  7. From R(x) AND Q(x) [assuming THERE EXISTS X: (R(X) AND Q(X)), setting x s.t. R(x) AND Q(x)], R(x) IMPLIES P(x) [assuming THERE EXISTS X: (R(X) AND Q(X)), setting x s.t. R(x) AND Q(x)]: deduce P(x) AND Q(x) [assuming THERE EXISTS X: (R(X) AND Q(X)), setting x s.t. R(x) AND Q(x)]. [EXERCISE 8.6(a)]
  8. From P(x) AND Q(x) [assuming THERE EXISTS X: (R(X) AND Q(X)), setting x s.t. R(x) AND Q(x)]: deduce THERE EXISTS X: (P(X) AND Q(X)) [assuming THERE EXISTS X: (R(X) AND Q(X)), setting x s.t. R(x) AND Q(x)]. [EXISTENTIAL INTRODUCTION]
  9. From THERE EXISTS X: (P(X) AND Q(X)) [assuming THERE EXISTS X: (R(X) AND Q(X)), setting x s.t. R(x) AND Q(x)]: deduce THERE EXISTS X: (P(X) AND Q(X)) [assuming THERE EXISTS X: (R(X) AND Q(X))]. [PULL]
  10. From NOT (THERE EXISTS X: (P(X) AND Q(X))): deduce NOT (THERE EXISTS X: (P(X) AND Q(X))) [assuming THERE EXISTS X: (R(X) AND Q(X))]. [PUSH]
  11. From THERE EXISTS X: (P(X) AND Q(X)) [assuming THERE EXISTS X: (R(X) AND Q(X))], NOT (THERE EXISTS X: (P(X) AND Q(X))) [assuming THERE EXISTS X: (R(X) AND Q(X))]: deduce NOT (THERE EXISTS X: (R(X) AND Q(X))). [REDUCTIO AD ABSURDUM (separated form)]
  12. QED!
DARII SYLLOGISM
  • An example of the Darii syllogism is "All rabbits have fur. Some pets are rabbits. Hence, some pets have fur.".
  1. FOR ALL X: (P(X) IMPLIES Q(X)). [given]
  2. THERE EXISTS X: (R(X) AND P(X)). [given]
  3. From THERE EXISTS X: (R(X) AND P(X)): deduce R(x) AND P(x) [setting x s.t. R(x) AND P(x)]. [EXISTENTIAL INSTANTIATION]
  4. From FOR ALL X: (P(X) IMPLIES Q(X)): deduce FOR ALL X: (P(X) IMPLIES Q(X)) [setting x s.t. R(x) AND P(x)]. [PUSH (for set variables)]
  5. From FOR ALL X: (P(X) IMPLIES Q(X)) [setting x s.t. R(x) AND P(x)]: deduce P(x) IMPLIES Q(x) [setting x s.t. R(x) AND P(x)]. [UNIVERSAL SPECIFICATION]
  6. From R(x) AND P(x) [setting x s.t. R(x) AND P(x)], P(x) IMPLIES Q(x) [setting x s.t. R(x) AND P(x)]: deduce R(x) AND Q(x) [setting x s.t. R(x) AND P(x)]. [EXERCISE 8.6(b)]
  7. From R(x) AND Q(x) [setting x s.t. R(x) AND P(x)]: deduce THERE EXISTS X: (R(X) AND Q(X)) [setting x s.t. R(x) AND P(x)]. [EXISTENTIAL INTRODUCTION]
  8. From THERE EXISTS X: (R(X) AND Q(X)) [setting x s.t. R(x) AND P(x)]: deduce THERE EXISTS X: (R(X) AND Q(X)). [PULL]
  9. QED!
FERIOQUE SYLLOGISM
  • An example of the Ferioque syllogism is "No homework is fun. Some reading is homework. Hence, some reading is not fun.".
  • Thanks to Anders Kaseorg for a short proof, Opax for a shorter proof, and Brian Quach for an even shorter proof.
  • For the purposes of matching, the formulae P(x), Q(x), R(x) should be ignored.
  1. NOT (THERE EXISTS X: (P(X) AND Q(X))). [given]
  2. THERE EXISTS X: (R(X) AND P(X)). [given]
  3. Deduce (NOT (THERE EXISTS X: (P(X) AND Q(X)))) IFF (FOR ALL X: (NOT (P(X) AND Q(X)))). [DE MORGAN'S LAW FOR QUANTIFIERS I]
  4. From NOT (THERE EXISTS X: (P(X) AND Q(X))), (NOT (THERE EXISTS X: (P(X) AND Q(X)))) IFF (FOR ALL X: (NOT (P(X) AND Q(X)))): deduce FOR ALL X: (NOT (P(X) AND Q(X))). [SUBSTITUTION]
  5. From FOR ALL X: (NOT (P(X) AND Q(X))): deduce NOT (P(x) AND Q(x)) [letting x be arbitrary]. [REVERSE UNIVERSAL INTRODUCTION]
  6. From NOT (P(x) AND Q(x)) [letting x be arbitrary]: deduce (NOT P(x)) OR (NOT Q(x)) [letting x be arbitrary]. [DE MORGAN'S LAW III]
  7. From (NOT P(x)) OR (NOT Q(x)) [letting x be arbitrary]: deduce P(x) IMPLIES (NOT Q(x)) [letting x be arbitrary]. [EXERCISE 12.4(b)]
  8. From P(x) IMPLIES (NOT Q(x)) [letting x be arbitrary]: deduce FOR ALL X: (P(X) IMPLIES (NOT Q(X))). [ UNIVERSAL INTRODUCTION]
  9. From FOR ALL X: (P(X) IMPLIES (NOT Q(X))), THERE EXISTS X: (R(X) AND P(X)): deduce THERE EXISTS X: (R(X) AND (NOT Q(X))). [DARII SYLLOGISM]
  10. QED!
BAROCO SYLLOGISM
  • An example of the Baroco syllogism is "All informative things are useful. Some websites are not useful. Hence, some websites are not informative.".
  • Thanks to Anders Kaseorg for a short proof, Opax for a shorter proof, and Brian Quach for an even shorter proof.
  1. FOR ALL X: (P(X) IMPLIES Q(X)). [given]
  2. THERE EXISTS X: (R(X) AND (NOT Q(X))). [given]
  3. From FOR ALL X: (P(X) IMPLIES Q(X)): deduce P(x) IMPLIES Q(x) [letting x be arbitrary]. [REVERSE UNIVERSAL INTRODUCTION]
  4. From P(x) IMPLIES Q(x) [letting x be arbitrary]: deduce (NOT Q(x)) IMPLIES (NOT P(x)) [letting x be arbitrary]. [CONTRAPOSITION]
  5. From (NOT Q(x)) IMPLIES (NOT P(x)) [letting x be arbitrary]: deduce FOR ALL X: ((NOT Q(X)) IMPLIES (NOT P(X))). [ UNIVERSAL INTRODUCTION]
  6. From FOR ALL X: ((NOT Q(X)) IMPLIES (NOT P(X))), THERE EXISTS X: (R(X) AND (NOT Q(X))): deduce THERE EXISTS X: (R(X) AND (NOT P(X))). [DARII SYLLOGISM]
  7. QED!
BOCARDO SYLLOGISM
  • An example of the Bocardo syllogism is "Some cats have no tails. All cats are mammals. Hence, some mammals have no tails.".
  • Thanks to Anders Kaseorg for a short proof.
  • For the purposes of matching, the formulae P(x), Q(x), R(x) should be ignored.
  1. THERE EXISTS X: (P(X) AND (NOT Q(X))). [given]
  2. FOR ALL X: (P(X) IMPLIES R(X)). [given]
  3. From THERE EXISTS X: (P(X) AND (NOT Q(X))): deduce P(x) AND (NOT Q(x)) [setting x s.t. P(x) AND (NOT Q(x))]. [EXISTENTIAL INSTANTIATION]
  4. From FOR ALL X: (P(X) IMPLIES R(X)): deduce FOR ALL X: (P(X) IMPLIES R(X)) [setting x s.t. P(x) AND (NOT Q(x))]. [PUSH (for set variables)]
  5. From FOR ALL X: (P(X) IMPLIES R(X)) [setting x s.t. P(x) AND (NOT Q(x))]: deduce P(x) IMPLIES R(x) [setting x s.t. P(x) AND (NOT Q(x))]. [UNIVERSAL SPECIFICATION]
  6. From P(x) AND (NOT Q(x)) [setting x s.t. P(x) AND (NOT Q(x))], P(x) IMPLIES R(x) [setting x s.t. P(x) AND (NOT Q(x))]: deduce R(x) AND (NOT Q(x)) [setting x s.t. P(x) AND (NOT Q(x))]. [EXERCISE 8.6(a)]
  7. From R(x) AND (NOT Q(x)) [setting x s.t. P(x) AND (NOT Q(x))]: deduce THERE EXISTS X: (R(X) AND (NOT Q(X))) [setting x s.t. P(x) AND (NOT Q(x))]. [EXISTENTIAL INTRODUCTION]
  8. From THERE EXISTS X: (R(X) AND (NOT Q(X))) [setting x s.t. P(x) AND (NOT Q(x))]: deduce THERE EXISTS X: (R(X) AND (NOT Q(X))). [PULL]
  9. QED!
BARBARI SYLLOGISM
  • In contrast to the syllogisms in Exercise 22.4, these syllogisms require a third assumption, namely the existence of some class of object. As such, they are sometimes not considered to be genuine syllogisms in the classical sense by some authors.
  • An example of the Barbari syllogism is "All men are mortal. All Greeks are men. Greeks exist. Hence, some Greeks are mortal."
  • Thanks to Anders Kaseorg for a short proof, and Brian Quach for a shorter proof.
  1. FOR ALL X: (P(X) IMPLIES Q(X)). [given]
  2. FOR ALL X: (Q(X) IMPLIES R(X)). [given]
  3. THERE EXISTS X: P(X). [given]
  4. From THERE EXISTS X: P(X): deduce P(x) [setting x s.t. P(x)]. [EXISTENTIAL INSTANTIATION]
  5. From P(x) [setting x s.t. P(x)]: deduce P(x) AND P(x) [setting x s.t. P(x)]. [AND IS IDEMPOTENT]
  6. From P(x) AND P(x) [setting x s.t. P(x)]: deduce THERE EXISTS X: (P(X) AND P(X)) [setting x s.t. P(x)]. [EXISTENTIAL INTRODUCTION]
  7. From THERE EXISTS X: (P(X) AND P(X)) [setting x s.t. P(x)]: deduce THERE EXISTS X: (P(X) AND P(X)). [PULL]
  8. From FOR ALL X: (P(X) IMPLIES Q(X)), THERE EXISTS X: (P(X) AND P(X)): deduce THERE EXISTS X: (P(X) AND Q(X)). [DARII SYLLOGISM]
  9. From FOR ALL X: (Q(X) IMPLIES R(X)), THERE EXISTS X: (P(X) AND Q(X)): deduce THERE EXISTS X: (P(X) AND R(X)). [DARII SYLLOGISM]
  10. QED!
CELARONT SYLLOGISM
  • An example of the Celaront syllogism is "No reptiles have fur. All snakes are reptiles. Snakes exist. Hence, some snakes have no fur."
  • For the purposes of matching, the formulae P(x), Q(x), R(x) should be ignored.
  • Thanks to Anders Kaseorg for a short proof, Lucas Silve for a shorter proof, and Brian Quach for an even shorter proof.
  1. NOT (THERE EXISTS X: (P(X) AND Q(X))). [given]
  2. FOR ALL X: (R(X) IMPLIES P(X)). [given]
  3. THERE EXISTS X: R(X). [given]
  4. From THERE EXISTS X: R(X): deduce R(x) [setting x s.t. R(x)]. [EXISTENTIAL INSTANTIATION]
  5. From R(x) [setting x s.t. R(x)]: deduce R(x) AND R(x) [setting x s.t. R(x)]. [AND IS IDEMPOTENT]
  6. From R(x) AND R(x) [setting x s.t. R(x)]: deduce THERE EXISTS X: (R(X) AND R(X)) [setting x s.t. R(x)]. [EXISTENTIAL INTRODUCTION]
  7. From THERE EXISTS X: (R(X) AND R(X)) [setting x s.t. R(x)]: deduce THERE EXISTS X: (R(X) AND R(X)). [PULL]
  8. From FOR ALL X: (R(X) IMPLIES P(X)), THERE EXISTS X: (R(X) AND R(X)): deduce THERE EXISTS X: (R(X) AND P(X)). [DARII SYLLOGISM]
  9. From NOT (THERE EXISTS X: (P(X) AND Q(X))), THERE EXISTS X: (R(X) AND P(X)): deduce THERE EXISTS X: (R(X) AND (NOT Q(X))). [FERIOQUE SYLLOGISM]
  10. QED!
CAMESTROS SYLLOGISM
  • An example of the Camestros syllogism is "All horses have hooves. No humans have hooves. Humans exist. Hence, some humans are not horses."
  • Thanks to Anders Kaseorg for a short proof, and Brian Quach for an even shorter proof.
  • For the purposes of matching, the formulae P(x), Q(x), R(x) should be ignored.
  1. FOR ALL X: (P(X) IMPLIES Q(X)). [given]
  2. NOT (THERE EXISTS X: (R(X) AND Q(X))). [given]
  3. THERE EXISTS X: R(X). [given]
  4. From THERE EXISTS X: R(X): deduce R(x) [setting x s.t. R(x)]. [EXISTENTIAL INSTANTIATION]
  5. From R(x) [setting x s.t. R(x)]: deduce R(x) AND R(x) [setting x s.t. R(x)]. [AND IS IDEMPOTENT]
  6. From R(x) AND R(x) [setting x s.t. R(x)]: deduce THERE EXISTS X: (R(X) AND R(X)) [setting x s.t. R(x)]. [EXISTENTIAL INTRODUCTION]
  7. From THERE EXISTS X: (R(X) AND R(X)) [setting x s.t. R(x)]: deduce THERE EXISTS X: (R(X) AND R(X)). [PULL]
  8. From NOT (THERE EXISTS X: (R(X) AND Q(X))), THERE EXISTS X: (R(X) AND R(X)): deduce THERE EXISTS X: (R(X) AND (NOT Q(X))). [FERIOQUE SYLLOGISM]
  9. From FOR ALL X: (P(X) IMPLIES Q(X)), THERE EXISTS X: (R(X) AND (NOT Q(X))): deduce THERE EXISTS X: (R(X) AND (NOT P(X))). [BAROCO SYLLOGISM]
  10. QED!
FELAPTON SYLLOGISM
  • An example of the Felapton syllogism is "No flowers are animals. All flowers are plants. Flowers exist. Hence, some plants are not animals."
  • For the purposes of matching, the formulae P(x), Q(x), R(x) should be ignored.
  • Thanks to Anders Kaseorg for a short proof, and Brian Quach for a shorter proof.
  1. NOT (THERE EXISTS X: (P(X) AND Q(X))). [given]
  2. FOR ALL X: (P(X) IMPLIES R(X)). [given]
  3. THERE EXISTS X: P(X). [given]
  4. From THERE EXISTS X: P(X): deduce P(x) [setting x s.t. P(x)]. [EXISTENTIAL INSTANTIATION]
  5. From P(x) [setting x s.t. P(x)]: deduce P(x) AND P(x) [setting x s.t. P(x)]. [AND IS IDEMPOTENT]
  6. From P(x) AND P(x) [setting x s.t. P(x)]: deduce THERE EXISTS X: (P(X) AND P(X)) [setting x s.t. P(x)]. [EXISTENTIAL INTRODUCTION]
  7. From THERE EXISTS X: (P(X) AND P(X)) [setting x s.t. P(x)]: deduce THERE EXISTS X: (P(X) AND P(X)). [PULL]
  8. From NOT (THERE EXISTS X: (P(X) AND Q(X))), THERE EXISTS X: (P(X) AND P(X)): deduce THERE EXISTS X: (P(X) AND (NOT Q(X))). [FERIOQUE SYLLOGISM]
  9. From THERE EXISTS X: (P(X) AND (NOT Q(X))), FOR ALL X: (P(X) IMPLIES R(X)): deduce THERE EXISTS X: (R(X) AND (NOT Q(X))). [BOCARDO SYLLOGISM]
  10. QED!
DARAPTI SYLLOGISM
  • An example of the Darapti syllogism is "All squares are rectangles. All squares are rhombi. Squares exist. Hence, some rhombi are rectangles."
  • Thanks to Anders Kaseorg for a short proof, and Brian Quach for a shorter proof.
  1. FOR ALL X: (P(X) IMPLIES Q(X)). [given]
  2. FOR ALL X: (P(X) IMPLIES R(X)). [given]
  3. THERE EXISTS X: P(X). [given]
  4. From THERE EXISTS X: P(X): deduce P(x) [setting x s.t. P(x)]. [EXISTENTIAL INSTANTIATION]
  5. From FOR ALL X: (P(X) IMPLIES R(X)): deduce FOR ALL X: (P(X) IMPLIES R(X)) [setting x s.t. P(x)]. [PUSH (for set variables)]
  6. From FOR ALL X: (P(X) IMPLIES R(X)) [setting x s.t. P(x)], P(x) [setting x s.t. P(x)]: deduce R(x) [setting x s.t. P(x)]. [BARBARA SYLLOGISM (singular form)]
  7. From R(x) [setting x s.t. P(x)], P(x) [setting x s.t. P(x)]: deduce R(x) AND P(x) [setting x s.t. P(x)]. [CONJUNCTION INTRODUCTION]
  8. From R(x) AND P(x) [setting x s.t. P(x)]: deduce THERE EXISTS X: (R(X) AND P(X)) [setting x s.t. P(x)]. [EXISTENTIAL INTRODUCTION]
  9. From THERE EXISTS X: (R(X) AND P(X)) [setting x s.t. P(x)]: deduce THERE EXISTS X: (R(X) AND P(X)). [PULL]
  10. From FOR ALL X: (P(X) IMPLIES Q(X)), THERE EXISTS X: (R(X) AND P(X)): deduce THERE EXISTS X: (R(X) AND Q(X)). [DARII SYLLOGISM]
  11. QED!
THERE EXISTS IS COMMUTATIVE
  • In this exercise you may need to use the law of existential instantiation with a specific choice of bound variable (rather than let the text choose the first available bound variable). In order to do so, one needs to click on the original statement P(α), then CTRL-click on the term α, then CTRL-click on the bound variable. (Alternatively, one can drag the statement to the term and then CTRL-click on the bound variable.)
  1. THERE EXISTS Y: (THERE EXISTS X: Q(X, Y)). [given]
  2. From THERE EXISTS Y: (THERE EXISTS X: Q(X, Y)): deduce THERE EXISTS X: Q(X, x) [setting x s.t. THERE EXISTS X: Q(X, x)]. [EXISTENTIAL INSTANTIATION]
  3. From THERE EXISTS X: Q(X, x) [setting x s.t. THERE EXISTS X: Q(X, x)]: deduce Q(y, x) [setting x s.t. THERE EXISTS X: Q(X, x), setting y s.t. Q(y, x)]. [EXISTENTIAL INSTANTIATION]
  4. From Q(y, x) [setting x s.t. THERE EXISTS X: Q(X, x), setting y s.t. Q(y, x)]: deduce THERE EXISTS Y: Q(y, Y) [setting x s.t. THERE EXISTS X: Q(X, x), setting y s.t. Q(y, x)]. [EXISTENTIAL INTRODUCTION]
  5. From THERE EXISTS Y: Q(y, Y) [setting x s.t. THERE EXISTS X: Q(X, x), setting y s.t. Q(y, x)]: deduce THERE EXISTS X: (THERE EXISTS Y: Q(X, Y)) [setting x s.t. THERE EXISTS X: Q(X, x), setting y s.t. Q(y, x)]. [EXISTENTIAL INTRODUCTION]
  6. From THERE EXISTS X: (THERE EXISTS Y: Q(X, Y)) [setting x s.t. THERE EXISTS X: Q(X, x), setting y s.t. Q(y, x)]: deduce THERE EXISTS X: (THERE EXISTS Y: Q(X, Y)). [DOUBLE PULL]
  7. QED!
INTERCHANGING FOR ALL AND THERE EXISTS
  • This exercise cannot be reversed. For instance, using the natural numbers as the domain of discourse, the statement "FOR ALL X: THERE EXISTS Y: Y>X" is true (every number has another number larger than it), but the statement "THERE EXISTS Y: FOR ALL X: Y>X" is false (there is no number that is larger than every number).
  • Thanks to Anders Kaseorg for a short proof.
  1. THERE EXISTS Y: (FOR ALL X: Q(X, Y)). [given]
  2. From THERE EXISTS Y: (FOR ALL X: Q(X, Y)): deduce FOR ALL X: Q(X, y) [setting y s.t. FOR ALL X: Q(X, y)]. [EXISTENTIAL INSTANTIATION]
  3. From FOR ALL X: Q(X, y) [setting y s.t. FOR ALL X: Q(X, y)]: deduce Q(x, y) [setting y s.t. FOR ALL X: Q(X, y), letting x be arbitrary]. [REVERSE UNIVERSAL INTRODUCTION]
  4. From Q(x, y) [setting y s.t. FOR ALL X: Q(X, y), letting x be arbitrary]: deduce THERE EXISTS Y: Q(x, Y) [setting y s.t. FOR ALL X: Q(X, y), letting x be arbitrary]. [EXISTENTIAL INTRODUCTION]
  5. From THERE EXISTS Y: Q(x, Y) [setting y s.t. FOR ALL X: Q(X, y), letting x be arbitrary]: deduce FOR ALL X: (THERE EXISTS Y: Q(X, Y)) [setting y s.t. FOR ALL X: Q(X, y)]. [ UNIVERSAL INTRODUCTION]
  6. From FOR ALL X: (THERE EXISTS Y: Q(X, Y)) [setting y s.t. FOR ALL X: Q(X, y)]: deduce FOR ALL X: (THERE EXISTS Y: Q(X, Y)). [PULL]
  7. QED!
This is the existential counterpart of Exercise 18.1.
  1. THERE EXISTS X: P(X). [given]
  2. From THERE EXISTS X: P(X): deduce P(x) [setting x s.t. P(x)]. [EXISTENTIAL INSTANTIATION]
  3. From P(x) [setting x s.t. P(x)]: deduce THERE EXISTS Y: P(Y) [setting x s.t. P(x)]. [EXISTENTIAL INTRODUCTION]
  4. From THERE EXISTS Y: P(Y) [setting x s.t. P(x)]: deduce THERE EXISTS Y: P(Y). [PULL]
  5. QED!
  • Technical note: matching for this exercise has not yet been implemented.
  1. Deduce (THERE EXISTS X: P(X)) AND (THERE EXISTS Y: Q(Y)) [assuming (THERE EXISTS X: P(X)) AND (THERE EXISTS Y: Q(Y))]. [IMPLICATION INTRODUCTION]
  2. From (THERE EXISTS X: P(X)) AND (THERE EXISTS Y: Q(Y)) [assuming (THERE EXISTS X: P(X)) AND (THERE EXISTS Y: Q(Y))]: deduce THERE EXISTS X: P(X) [assuming (THERE EXISTS X: P(X)) AND (THERE EXISTS Y: Q(Y))]. [CONJUNCTION ELIMINATION (left)]
  3. From (THERE EXISTS X: P(X)) AND (THERE EXISTS Y: Q(Y)) [assuming (THERE EXISTS X: P(X)) AND (THERE EXISTS Y: Q(Y))]: deduce THERE EXISTS Y: Q(Y) [assuming (THERE EXISTS X: P(X)) AND (THERE EXISTS Y: Q(Y))]. [CONJUNCTION ELIMINATION (right)]
  4. From THERE EXISTS X: P(X) [assuming (THERE EXISTS X: P(X)) AND (THERE EXISTS Y: Q(Y))]: deduce P(x) [assuming (THERE EXISTS X: P(X)) AND (THERE EXISTS Y: Q(Y)), setting x s.t. P(x)]. [EXISTENTIAL INSTANTIATION]
  5. From THERE EXISTS Y: Q(Y) [assuming (THERE EXISTS X: P(X)) AND (THERE EXISTS Y: Q(Y))]: deduce THERE EXISTS Y: Q(Y) [assuming (THERE EXISTS X: P(X)) AND (THERE EXISTS Y: Q(Y)), setting x s.t. P(x)]. [PUSH (for set variables)]
  6. From THERE EXISTS Y: Q(Y) [assuming (THERE EXISTS X: P(X)) AND (THERE EXISTS Y: Q(Y)), setting x s.t. P(x)]: deduce Q(y) [assuming (THERE EXISTS X: P(X)) AND (THERE EXISTS Y: Q(Y)), setting x s.t. P(x), setting y s.t. Q(y)]. [EXISTENTIAL INSTANTIATION]
  7. From P(x) [assuming (THERE EXISTS X: P(X)) AND (THERE EXISTS Y: Q(Y)), setting x s.t. P(x)]: deduce P(x) [assuming (THERE EXISTS X: P(X)) AND (THERE EXISTS Y: Q(Y)), setting x s.t. P(x), setting y s.t. Q(y)]. [PUSH (for set variables)]
  8. From P(x) [assuming (THERE EXISTS X: P(X)) AND (THERE EXISTS Y: Q(Y)), setting x s.t. P(x), setting y s.t. Q(y)], Q(y) [assuming (THERE EXISTS X: P(X)) AND (THERE EXISTS Y: Q(Y)), setting x s.t. P(x), setting y s.t. Q(y)]: deduce P(x) AND Q(y) [assuming (THERE EXISTS X: P(X)) AND (THERE EXISTS Y: Q(Y)), setting x s.t. P(x), setting y s.t. Q(y)]. [CONJUNCTION INTRODUCTION]
  9. From P(x) AND Q(y) [assuming (THERE EXISTS X: P(X)) AND (THERE EXISTS Y: Q(Y)), setting x s.t. P(x), setting y s.t. Q(y)]: deduce THERE EXISTS Y: (P(x) AND Q(Y)) [assuming (THERE EXISTS X: P(X)) AND (THERE EXISTS Y: Q(Y)), setting x s.t. P(x), setting y s.t. Q(y)]. [EXISTENTIAL INTRODUCTION]
  10. From THERE EXISTS Y: (P(x) AND Q(Y)) [assuming (THERE EXISTS X: P(X)) AND (THERE EXISTS Y: Q(Y)), setting x s.t. P(x), setting y s.t. Q(y)]: deduce THERE EXISTS X: (THERE EXISTS Y: (P(X) AND Q(Y))) [assuming (THERE EXISTS X: P(X)) AND (THERE EXISTS Y: Q(Y)), setting x s.t. P(x), setting y s.t. Q(y)]. [EXISTENTIAL INTRODUCTION]
  11. From THERE EXISTS X: (THERE EXISTS Y: (P(X) AND Q(Y))) [assuming (THERE EXISTS X: P(X)) AND (THERE EXISTS Y: Q(Y)), setting x s.t. P(x), setting y s.t. Q(y)]: deduce THERE EXISTS X: (THERE EXISTS Y: (P(X) AND Q(Y))) [assuming (THERE EXISTS X: P(X)) AND (THERE EXISTS Y: Q(Y))]. [DOUBLE PULL]
  12. Deduce THERE EXISTS X: (THERE EXISTS Y: (P(X) AND Q(Y))) [assuming THERE EXISTS X: (THERE EXISTS Y: (P(X) AND Q(Y)))]. [IMPLICATION INTRODUCTION]
  13. From THERE EXISTS X: (THERE EXISTS Y: (P(X) AND Q(Y))) [assuming THERE EXISTS X: (THERE EXISTS Y: (P(X) AND Q(Y)))]: deduce THERE EXISTS Y: (P(x) AND Q(Y)) [assuming THERE EXISTS X: (THERE EXISTS Y: (P(X) AND Q(Y))), setting x s.t. THERE EXISTS Y: (P(x) AND Q(Y))]. [EXISTENTIAL INSTANTIATION]
  14. From THERE EXISTS Y: (P(x) AND Q(Y)) [assuming THERE EXISTS X: (THERE EXISTS Y: (P(X) AND Q(Y))), setting x s.t. THERE EXISTS Y: (P(x) AND Q(Y))]: deduce P(x) AND Q(y) [assuming THERE EXISTS X: (THERE EXISTS Y: (P(X) AND Q(Y))), setting x s.t. THERE EXISTS Y: (P(x) AND Q(Y)), setting y s.t. P(x) AND Q(y)]. [EXISTENTIAL INSTANTIATION]
  15. From P(x) AND Q(y) [assuming THERE EXISTS X: (THERE EXISTS Y: (P(X) AND Q(Y))), setting x s.t. THERE EXISTS Y: (P(x) AND Q(Y)), setting y s.t. P(x) AND Q(y)]: deduce P(x) [assuming THERE EXISTS X: (THERE EXISTS Y: (P(X) AND Q(Y))), setting x s.t. THERE EXISTS Y: (P(x) AND Q(Y)), setting y s.t. P(x) AND Q(y)]. [CONJUNCTION ELIMINATION (left)]
  16. From P(x) AND Q(y) [assuming THERE EXISTS X: (THERE EXISTS Y: (P(X) AND Q(Y))), setting x s.t. THERE EXISTS Y: (P(x) AND Q(Y)), setting y s.t. P(x) AND Q(y)]: deduce Q(y) [assuming THERE EXISTS X: (THERE EXISTS Y: (P(X) AND Q(Y))), setting x s.t. THERE EXISTS Y: (P(x) AND Q(Y)), setting y s.t. P(x) AND Q(y)]. [CONJUNCTION ELIMINATION (right)]
  17. From P(x) [assuming THERE EXISTS X: (THERE EXISTS Y: (P(X) AND Q(Y))), setting x s.t. THERE EXISTS Y: (P(x) AND Q(Y)), setting y s.t. P(x) AND Q(y)]: deduce THERE EXISTS X: P(X) [assuming THERE EXISTS X: (THERE EXISTS Y: (P(X) AND Q(Y))), setting x s.t. THERE EXISTS Y: (P(x) AND Q(Y)), setting y s.t. P(x) AND Q(y)]. [EXISTENTIAL INTRODUCTION]
  18. From Q(y) [assuming THERE EXISTS X: (THERE EXISTS Y: (P(X) AND Q(Y))), setting x s.t. THERE EXISTS Y: (P(x) AND Q(Y)), setting y s.t. P(x) AND Q(y)]: deduce THERE EXISTS Y: Q(Y) [assuming THERE EXISTS X: (THERE EXISTS Y: (P(X) AND Q(Y))), setting x s.t. THERE EXISTS Y: (P(x) AND Q(Y)), setting y s.t. P(x) AND Q(y)]. [EXISTENTIAL INTRODUCTION]
  19. From THERE EXISTS X: P(X) [assuming THERE EXISTS X: (THERE EXISTS Y: (P(X) AND Q(Y))), setting x s.t. THERE EXISTS Y: (P(x) AND Q(Y)), setting y s.t. P(x) AND Q(y)], THERE EXISTS Y: Q(Y) [assuming THERE EXISTS X: (THERE EXISTS Y: (P(X) AND Q(Y))), setting x s.t. THERE EXISTS Y: (P(x) AND Q(Y)), setting y s.t. P(x) AND Q(y)]: deduce (THERE EXISTS X: P(X)) AND (THERE EXISTS Y: Q(Y)) [assuming THERE EXISTS X: (THERE EXISTS Y: (P(X) AND Q(Y))), setting x s.t. THERE EXISTS Y: (P(x) AND Q(Y)), setting y s.t. P(x) AND Q(y)]. [CONJUNCTION INTRODUCTION]
  20. From (THERE EXISTS X: P(X)) AND (THERE EXISTS Y: Q(Y)) [assuming THERE EXISTS X: (THERE EXISTS Y: (P(X) AND Q(Y))), setting x s.t. THERE EXISTS Y: (P(x) AND Q(Y)), setting y s.t. P(x) AND Q(y)]: deduce (THERE EXISTS X: P(X)) AND (THERE EXISTS Y: Q(Y)) [assuming THERE EXISTS X: (THERE EXISTS Y: (P(X) AND Q(Y)))]. [DOUBLE PULL]
  21. From (THERE EXISTS X: P(X)) AND (THERE EXISTS Y: Q(Y)) [assuming THERE EXISTS X: (THERE EXISTS Y: (P(X) AND Q(Y)))], THERE EXISTS X: (THERE EXISTS Y: (P(X) AND Q(Y))) [assuming (THERE EXISTS X: P(X)) AND (THERE EXISTS Y: Q(Y))]: deduce ((THERE EXISTS X: P(X)) AND (THERE EXISTS Y: Q(Y))) IFF (THERE EXISTS X: (THERE EXISTS Y: (P(X) AND Q(Y)))). [BICONDITIONAL INTRODUCTION (ASSUMPTION FORM)]
  22. QED!
LEWIS CARROLL SYLLOGISM
  • Lewis Carroll is best known for his books "Alice in Wonderland" and "Through the Looking Glass". But he also wrote a list of logic puzzles, some of which can be found here.
  • The simplest of his logic puzzles is the following. Given the hypotheses "Babies are illogical. Illogical persons are despised. Nobody who is despised can manage a crocodile", conclude "Babies cannot handle crocodiles".
  • The exercise here is a translation of that puzzle to first-order logic - can you see how?
  • Thanks to Anders Kaseorg for a short proof, Opax for a shorter proof, Anders Kaseorg for an even shorter proof, and Brian Quach for a yet shorter proof.
  • For the purposes of applying this exercise, the formulae P(x), Q(x), R(x), S(x) should be ignored.
  1. FOR ALL X: (P(X) IMPLIES (NOT Q(X))). [given]
  2. FOR ALL X: ((NOT Q(X)) IMPLIES R(X)). [given]
  3. NOT (THERE EXISTS X: (R(X) AND S(X))). [given]
  4. From NOT (THERE EXISTS X: (R(X) AND S(X))), FOR ALL X: ((NOT Q(X)) IMPLIES R(X)): deduce NOT (THERE EXISTS X: ((NOT Q(X)) AND S(X))). [CELARENT SYLLOGISM]
  5. Deduce (NOT (THERE EXISTS X: ((NOT Q(X)) AND S(X)))) IFF (FOR ALL X: (NOT ((NOT Q(X)) AND S(X)))). [DE MORGAN'S LAW FOR QUANTIFIERS I]
  6. From NOT (THERE EXISTS X: ((NOT Q(X)) AND S(X))), (NOT (THERE EXISTS X: ((NOT Q(X)) AND S(X)))) IFF (FOR ALL X: (NOT ((NOT Q(X)) AND S(X)))): deduce FOR ALL X: (NOT ((NOT Q(X)) AND S(X))). [SUBSTITUTION]
  7. From FOR ALL X: (NOT ((NOT Q(X)) AND S(X))): deduce NOT ((NOT Q(x)) AND S(x)) [letting x be arbitrary]. [REVERSE UNIVERSAL INTRODUCTION]
  8. From NOT ((NOT Q(x)) AND S(x)) [letting x be arbitrary]: deduce (NOT (NOT Q(x))) OR (NOT S(x)) [letting x be arbitrary]. [DE MORGAN'S LAW III]
  9. From (NOT (NOT Q(x))) OR (NOT S(x)) [letting x be arbitrary]: deduce (NOT Q(x)) IMPLIES (NOT S(x)) [letting x be arbitrary]. [EXERCISE 12.4(b)]
  10. From (NOT Q(x)) IMPLIES (NOT S(x)) [letting x be arbitrary]: deduce FOR ALL X: ((NOT Q(X)) IMPLIES (NOT S(X))). [ UNIVERSAL INTRODUCTION]
  11. From FOR ALL X: ((NOT Q(X)) IMPLIES (NOT S(X))), FOR ALL X: (P(X) IMPLIES (NOT Q(X))): deduce FOR ALL X: (P(X) IMPLIES (NOT S(X))). [BARBARA SYLLOGISM (classical form)]
  12. QED!
  • In previous exercises, formulas such as Q(x,y) were manually provided for those exercises where they were needed. In this section, a new window has been unlocked that allows one to generate such formulas without manual intervention.
  • The Predicates window contains all the predicates that appear in the exercise. Predicates can be take one or more arguments, indicated here by em-dashes —.
  • A few exercises from now, we will also introduce operators, which are similar to predicates and which will appear in the Operators window.
  • If one drags a term to each argument of a predicate, one creates a formula in the Formulas window (and the arguments of the predicate are then reset to em-dashes). For instance, to create the formula Q(x,y), drag the term x to the first argument of Q(—,—), and drag the term y to the second argument.
  • Technical note: matching for this exercise has not yet been implemented.
  1. Form environment [letting x be arbitrary]. [FREE VARIABLE INTRODUCTION]
  2. Form environment [letting x, y be arbitrary]. [FREE VARIABLE INTRODUCTION]
  3. Deduce Q(x, y) IMPLIES Q(x, y) [letting x, y be arbitrary]. [IMPLIES IS IDEMPOTENT]
  4. From Q(x, y) IMPLIES Q(x, y) [letting x, y be arbitrary]: deduce FOR ALL Y: (Q(x, Y) IMPLIES Q(x, Y)) [letting x be arbitrary]. [ UNIVERSAL INTRODUCTION]
  5. From FOR ALL Y: (Q(x, Y) IMPLIES Q(x, Y)) [letting x be arbitrary]: deduce FOR ALL X: (FOR ALL Y: (Q(X, Y) IMPLIES Q(X, Y))). [ UNIVERSAL INTRODUCTION]
  6. QED!
  • Some predicates are customarily written in between their arguments, rather than to the left of the arguments. The most familiar examples of these are the comparison predicates <, >, ≤, ≥ and the equality relation =.
  • However, this difference is purely notational, and these predicates otherwise follow all the laws of first-order logic that predicates such as Q(—, —) do.
  • Technical note: matching for this exercise has not yet been implemented.
  1. Form environment [letting x be arbitrary]. [FREE VARIABLE INTRODUCTION]
  2. Form environment [letting x, y be arbitrary]. [FREE VARIABLE INTRODUCTION]
  3. Deduce (x > y) IMPLIES (x > y) [letting x, y be arbitrary]. [IMPLIES IS IDEMPOTENT]
  4. From (x > y) IMPLIES (x > y) [letting x, y be arbitrary]: deduce FOR ALL Y: ((x > Y) IMPLIES (x > Y)) [letting x be arbitrary]. [ UNIVERSAL INTRODUCTION]
  5. From FOR ALL Y: ((x > Y) IMPLIES (x > Y)) [letting x be arbitrary]: deduce FOR ALL X: (FOR ALL Y: ((X > Y) IMPLIES (X > Y))). [ UNIVERSAL INTRODUCTION]
  6. QED!
  • In addition to predicates, first-order logic also allows the use of operators, also known as function symbols.
  • operators are symbols that take some number of terms to produce more complicated terms. The most familiar examples of operators are the arithmetic operators +, -, x, /; thus for instance one could take the terms x and y and produce a new term x+y.
  • Operators closely resemble predicates, except that a predicate produces formulas, whereas an operator produces terms.
  • As such, we place operators an Operators window similar to the Predicates window as predicates; the only difference is that the output of such operators goes into the Terms window rather than the Formulas window.
  • Note that compound terms such as x+y are not free variables or bound variables, and so cannot be used for those laws of first-order logic that require such variables. However, they are still perfectly good terms for use in such laws as universal specification or existential introduction.
  • Technical note: matching for this exercise has not yet been implemented.
  1. Form environment [letting x be arbitrary]. [FREE VARIABLE INTRODUCTION]
  2. Form environment [letting x, y be arbitrary]. [FREE VARIABLE INTRODUCTION]
  3. Deduce P(x + y) IMPLIES P(x + y) [letting x, y be arbitrary]. [IMPLIES IS IDEMPOTENT]
  4. From P(x + y) IMPLIES P(x + y) [letting x, y be arbitrary]: deduce FOR ALL Y: (P(x + Y) IMPLIES P(x + Y)) [letting x be arbitrary]. [ UNIVERSAL INTRODUCTION]
  5. From FOR ALL Y: (P(x + Y) IMPLIES P(x + Y)) [letting x be arbitrary]: deduce FOR ALL X: (FOR ALL Y: (P(X + Y) IMPLIES P(X + Y))). [ UNIVERSAL INTRODUCTION]
  6. QED!
RUSSELL'S PARADOX
  • Russell's paradox is a famous paradox in set theory. It asserts that there cannot exist a set that consists precisely of those sets that do not contain themselves.
  • It had a significant impact in set theory, showing that certain axioms of "naive set theory" were in fact inconsistent. This eventually led to modern axiomatisations of set theory, such as Zermelo-Fraenkel-Choice (ZFC).
  • An informal version of the paradox involves a barber who shaves everyone who does not shave themselves. Who shaves the barber?
  • Thanks to Anders Kaseorg for a short proof.
  • Technical note: matching for this exercise has not yet been implemented.
  1. THERE EXISTS X: (FOR ALL Y: ((Y ∈ X) IFF (NOT (Y ∈ Y)))). [given]
  2. From THERE EXISTS X: (FOR ALL Y: ((Y ∈ X) IFF (NOT (Y ∈ Y)))): deduce FOR ALL Y: ((Y ∈ x) IFF (NOT (Y ∈ Y))) [setting x s.t. FOR ALL Y: ((Y ∈ x) IFF (NOT (Y ∈ Y)))]. [EXISTENTIAL INSTANTIATION]
  3. From FOR ALL Y: ((Y ∈ x) IFF (NOT (Y ∈ Y))) [setting x s.t. FOR ALL Y: ((Y ∈ x) IFF (NOT (Y ∈ Y)))]: deduce (x ∈ x) IFF (NOT (x ∈ x)) [setting x s.t. FOR ALL Y: ((Y ∈ x) IFF (NOT (Y ∈ Y)))]. [UNIVERSAL SPECIFICATION]
  4. From (x ∈ x) IFF (NOT (x ∈ x)) [setting x s.t. FOR ALL Y: ((Y ∈ x) IFF (NOT (Y ∈ Y)))]: deduce (x ∈ x) IMPLIES (NOT (x ∈ x)) [setting x s.t. FOR ALL Y: ((Y ∈ x) IFF (NOT (Y ∈ Y)))]. [BICONDITIONAL ELIMINATION (left)]
  5. From (x ∈ x) IMPLIES (NOT (x ∈ x)) [setting x s.t. FOR ALL Y: ((Y ∈ x) IFF (NOT (Y ∈ Y)))]: deduce (NOT (x ∈ x)) OR (NOT (x ∈ x)) [setting x s.t. FOR ALL Y: ((Y ∈ x) IFF (NOT (Y ∈ Y)))]. [EXERCISE 12.4(a)]
  6. From (NOT (x ∈ x)) OR (NOT (x ∈ x)) [setting x s.t. FOR ALL Y: ((Y ∈ x) IFF (NOT (Y ∈ Y)))]: deduce NOT (x ∈ x) [setting x s.t. FOR ALL Y: ((Y ∈ x) IFF (NOT (Y ∈ Y)))]. [OR IS IDEMPOTENT (right)]
  7. From NOT (x ∈ x) [setting x s.t. FOR ALL Y: ((Y ∈ x) IFF (NOT (Y ∈ Y)))], (x ∈ x) IFF (NOT (x ∈ x)) [setting x s.t. FOR ALL Y: ((Y ∈ x) IFF (NOT (Y ∈ Y)))]: deduce NOT (NOT (x ∈ x)) [setting x s.t. FOR ALL Y: ((Y ∈ x) IFF (NOT (Y ∈ Y)))]. [SUBSTITUTION FOR NOT]
  8. From NOT (x ∈ x) [setting x s.t. FOR ALL Y: ((Y ∈ x) IFF (NOT (Y ∈ Y)))], NOT (NOT (x ∈ x)) [setting x s.t. FOR ALL Y: ((Y ∈ x) IFF (NOT (Y ∈ Y)))]: deduce (NOT (x ∈ x)) AND (NOT (NOT (x ∈ x))) [setting x s.t. FOR ALL Y: ((Y ∈ x) IFF (NOT (Y ∈ Y)))]. [CONJUNCTION INTRODUCTION]
  9. From (NOT (x ∈ x)) AND (NOT (NOT (x ∈ x))) [setting x s.t. FOR ALL Y: ((Y ∈ x) IFF (NOT (Y ∈ Y)))]: deduce NOT TRUE [setting x s.t. FOR ALL Y: ((Y ∈ x) IFF (NOT (Y ∈ Y)))]. [EX FALSO QUODLIBET]
  10. From NOT TRUE [setting x s.t. FOR ALL Y: ((Y ∈ x) IFF (NOT (Y ∈ Y)))]: deduce NOT TRUE. [PULL]
  11. QED!
NO LARGEST NATURAL NUMBER
  • If one takes the natural numbers as the domain of discourse, and interprets arithmetic symbols such as ≥, +, 1 in the usual fashion, then this exercise is asking you to prove that there is no natural number that is greater than or equal to all natural numbers. Your given information is that a natural number X is never greater than its successor X+1.
  • While one could solve this exercise by randomly trying various laws of deduction, it is better to use your mathematical intuition and think first about why the above assertion about natural numbers is true. Once you figure out why, convert your reasoning into a formal proof.
  • Technical note: matching for this exercise has not yet been implemented.
  1. FOR ALL X: (NOT (X ≥ (X + 1))). [given]
  2. Deduce THERE EXISTS X: (FOR ALL Y: (X ≥ Y)) [assuming THERE EXISTS X: (FOR ALL Y: (X ≥ Y))]. [IMPLICATION INTRODUCTION]
  3. From THERE EXISTS X: (FOR ALL Y: (X ≥ Y)) [assuming THERE EXISTS X: (FOR ALL Y: (X ≥ Y))]: deduce FOR ALL Y: (x ≥ Y) [assuming THERE EXISTS X: (FOR ALL Y: (X ≥ Y)), setting x s.t. FOR ALL Y: (x ≥ Y)]. [EXISTENTIAL INSTANTIATION]
  4. From FOR ALL Y: (x ≥ Y) [assuming THERE EXISTS X: (FOR ALL Y: (X ≥ Y)), setting x s.t. FOR ALL Y: (x ≥ Y)]: deduce x ≥ (x + 1) [assuming THERE EXISTS X: (FOR ALL Y: (X ≥ Y)), setting x s.t. FOR ALL Y: (x ≥ Y)]. [UNIVERSAL SPECIFICATION]
  5. From FOR ALL X: (NOT (X ≥ (X + 1))): deduce FOR ALL X: (NOT (X ≥ (X + 1))) [assuming THERE EXISTS X: (FOR ALL Y: (X ≥ Y)), setting x s.t. FOR ALL Y: (x ≥ Y)]. [DOUBLE PUSH (mixed III)]
  6. From FOR ALL X: (NOT (X ≥ (X + 1))) [assuming THERE EXISTS X: (FOR ALL Y: (X ≥ Y)), setting x s.t. FOR ALL Y: (x ≥ Y)]: deduce NOT (x ≥ (x + 1)) [assuming THERE EXISTS X: (FOR ALL Y: (X ≥ Y)), setting x s.t. FOR ALL Y: (x ≥ Y)]. [UNIVERSAL SPECIFICATION]
  7. From x ≥ (x + 1) [assuming THERE EXISTS X: (FOR ALL Y: (X ≥ Y)), setting x s.t. FOR ALL Y: (x ≥ Y)], NOT (x ≥ (x + 1)) [assuming THERE EXISTS X: (FOR ALL Y: (X ≥ Y)), setting x s.t. FOR ALL Y: (x ≥ Y)]: deduce (x ≥ (x + 1)) AND (NOT (x ≥ (x + 1))) [assuming THERE EXISTS X: (FOR ALL Y: (X ≥ Y)), setting x s.t. FOR ALL Y: (x ≥ Y)]. [CONJUNCTION INTRODUCTION]
  8. From (x ≥ (x + 1)) AND (NOT (x ≥ (x + 1))) [assuming THERE EXISTS X: (FOR ALL Y: (X ≥ Y)), setting x s.t. FOR ALL Y: (x ≥ Y)]: deduce TRUE AND (NOT TRUE) [assuming THERE EXISTS X: (FOR ALL Y: (X ≥ Y)), setting x s.t. FOR ALL Y: (x ≥ Y)]. [EX FALSO QUODLIBET]
  9. From TRUE AND (NOT TRUE) [assuming THERE EXISTS X: (FOR ALL Y: (X ≥ Y)), setting x s.t. FOR ALL Y: (x ≥ Y)]: deduce TRUE AND (NOT TRUE) [assuming THERE EXISTS X: (FOR ALL Y: (X ≥ Y))]. [PULL]
  10. From TRUE AND (NOT TRUE) [assuming THERE EXISTS X: (FOR ALL Y: (X ≥ Y))]: deduce NOT (THERE EXISTS X: (FOR ALL Y: (X ≥ Y))). [REDUCTIO AD ABSURDUM]
  11. QED!
EQUALITY IS SYMMETRIC
  • Amongst all the predicates in first-order logic, there is a special one that obeys special rules: the equality predicate =. This binary predicate is written as a relation, thus we write α=β rather than =(α,β).
  • Equality obeys two fundamental laws. The first is reflexivity: if α is a term, then the statement α=α is true (assuming of course that this statement is well-formed in the target environment.
  • The second law is the indiscernability of identicals (also known as Leibniz's law): if one knows that α=β, and one knows that P(α) is true, then one can conclude that P(β) is also true.
  • To use the law of reflexivity, click on a term in the Terms window, or drag a term into a target environment.
  • To use the indiscernability of identicals, drag an equation of the form α=β to another statement in the same environment.
  • As with the law of existential introduction, there can be multiple ways in which the indiscernability of identicals law can be applied to a given pair of statements. However, the game removes the "trivial" deduction of concluding a statement from itself.
  • With these two laws of equality, the the set of rules of deduction for first-order logic used in this text is now complete. (But this is not the only such set of rules; there are other deductive systems for first-order logic that use a different set of rules, though they still end up proving the same set of statements.)
  • The indiscernability of identicals works in mathematics, because mathematics is concerned almost exclusively with extensional statements. But in natural languages such as English, there are also intensional statements to which the indiscernability of identicals does not apply.
  1. α = β. [given]
  2. Deduce α = α. [EQUALITY IS REFLEXIVE]
  3. From α = α, α = β: deduce β = α. [INDISCERNABILITY OF IDENTICALS]
  4. QED!
EQUALITY IS TRANSITIVE
  • The fact that equality is reflexive, symmetric, and transitive can be summarised into the single observation that equality is an equivalence relation.
  1. α = β. [given]
  2. β = γ. [given]
  3. From α = β, β = γ: deduce α = γ. [INDISCERNABILITY OF IDENTICALS]
  4. QED!
SUBSTITUTION
  • Technical note: matching for this exercise has not yet been implemented.
  1. α = β. [given]
  2. Deduce f(α) = f(α). [EQUALITY IS REFLEXIVE]
  3. From f(α) = f(α), α = β: deduce f(α) = f(β). [INDISCERNABILITY OF IDENTICALS]
  4. QED!
LEFT IDENTITY EQUALS RIGHT IDENTITY
  • Now that all the laws of first-order logic are unlocked, it is now possible (in principle at least) to start proving statements in mathematics itself, rather than in logic.
  • We illustrate this with one of the first results in group theory: if one has a left-identity α (so that α * X = X for all X) and a right-identity β (so that X * β = X for all X), then α and β must be equal.
  • Technical note: matching for this exercise has not yet been implemented.
  1. FOR ALL X: ((α * X) = X). [given]
  2. FOR ALL X: ((X * β) = X). [given]
  3. From FOR ALL X: ((α * X) = X): deduce (α * β) = β. [UNIVERSAL SPECIFICATION]
  4. From FOR ALL X: ((X * β) = X): deduce (α * β) = α. [UNIVERSAL SPECIFICATION]
  5. From (α * β) = β, (α * β) = α: deduce α = β. [INDISCERNABILITY OF IDENTICALS]
  6. QED!
CANCELLATION LAW
  • This exercise asks to prove a more complicated result in group theory, namely the cancellation law that allows one to deduce the identity β = γ from α * β = α * γ when α, β, γ lie in a group.
  • There are three relevant group laws here. The first is identity: there is a term 1 such that 1*X=X for all group elements X.
  • The second is associativity: one has X*(Y*Z) = (X*Y)*Z for all group elements X,Y,Z.
  • The third is inverse: for every group element X, there is a group element Y such that Y*X=1.
  • This is a relatively easy exercise in group theory when written out in informal mathematical language, but turns out to be somewhat lengthy when one tries to formalise it in first-order logic. More generally, first-order logic tends to be too "low-level" of a proof system to be convenient for advanced mathematics; most proofs in mathematics are instead written in a more "high-level" fashion, using less formal, but more expressive, sentences in English (or in other languages) in place of the very limited sentences available to first-order logic.
  • Thanks to Gesse Roure for a short proof, and Anders Kaseorg for a shorter proof.
  • Technical note: matching for this exercise has not yet been implemented.
  1. FOR ALL X: ((1 * X) = X). [given]
  2. FOR ALL X: (FOR ALL Y: (FOR ALL Z: ((X * (Y * Z)) = ((X * Y) * Z)))). [given]
  3. FOR ALL X: (THERE EXISTS Y: ((Y * X) = 1)). [given]
  4. (α * β) = (α * γ). [given]
  5. From FOR ALL X: (THERE EXISTS Y: ((Y * X) = 1)): deduce THERE EXISTS Y: ((Y * α) = 1). [UNIVERSAL SPECIFICATION]
  6. From THERE EXISTS Y: ((Y * α) = 1): deduce (x * α) = 1 [setting x s.t. (x * α) = 1]. [EXISTENTIAL INSTANTIATION]
  7. From FOR ALL X: (FOR ALL Y: (FOR ALL Z: ((X * (Y * Z)) = ((X * Y) * Z)))): deduce FOR ALL X: (FOR ALL Y: (FOR ALL Z: ((X * (Y * Z)) = ((X * Y) * Z)))) [setting x s.t. (x * α) = 1]. [PUSH (for set variables)]
  8. From FOR ALL X: (FOR ALL Y: (FOR ALL Z: ((X * (Y * Z)) = ((X * Y) * Z)))) [setting x s.t. (x * α) = 1]: deduce FOR ALL Y: (FOR ALL Z: ((x * (Y * Z)) = ((x * Y) * Z))) [setting x s.t. (x * α) = 1]. [UNIVERSAL SPECIFICATION]
  9. From FOR ALL Y: (FOR ALL Z: ((x * (Y * Z)) = ((x * Y) * Z))) [setting x s.t. (x * α) = 1]: deduce FOR ALL Z: ((x * (α * Z)) = ((x * α) * Z)) [setting x s.t. (x * α) = 1]. [UNIVERSAL SPECIFICATION]
  10. From FOR ALL Z: ((x * (α * Z)) = ((x * α) * Z)) [setting x s.t. (x * α) = 1], (x * α) = 1 [setting x s.t. (x * α) = 1]: deduce FOR ALL Z: ((x * (α * Z)) = (1 * Z)) [setting x s.t. (x * α) = 1]. [INDISCERNABILITY OF IDENTICALS]
  11. From FOR ALL Z: ((x * (α * Z)) = (1 * Z)) [setting x s.t. (x * α) = 1]: deduce (x * (α * β)) = (1 * β) [setting x s.t. (x * α) = 1]. [UNIVERSAL SPECIFICATION]
  12. From (α * β) = (α * γ): deduce (α * β) = (α * γ) [setting x s.t. (x * α) = 1]. [PUSH (for set variables)]
  13. From (x * (α * β)) = (1 * β) [setting x s.t. (x * α) = 1], (α * β) = (α * γ) [setting x s.t. (x * α) = 1]: deduce (x * (α * γ)) = (1 * β) [setting x s.t. (x * α) = 1]. [INDISCERNABILITY OF IDENTICALS]
  14. From FOR ALL Z: ((x * (α * Z)) = (1 * Z)) [setting x s.t. (x * α) = 1]: deduce (x * (α * γ)) = (1 * γ) [setting x s.t. (x * α) = 1]. [UNIVERSAL SPECIFICATION]
  15. From (x * (α * γ)) = (1 * γ) [setting x s.t. (x * α) = 1], (x * (α * γ)) = (1 * β) [setting x s.t. (x * α) = 1]: deduce (1 * β) = (1 * γ) [setting x s.t. (x * α) = 1]. [INDISCERNABILITY OF IDENTICALS]
  16. From (1 * β) = (1 * γ) [setting x s.t. (x * α) = 1]: deduce (1 * β) = (1 * γ). [PULL]
  17. From FOR ALL X: ((1 * X) = X): deduce (1 * β) = β. [UNIVERSAL SPECIFICATION]
  18. From FOR ALL X: ((1 * X) = X): deduce (1 * γ) = γ. [UNIVERSAL SPECIFICATION]
  19. From (1 * β) = (1 * γ), (1 * β) = β: deduce β = (1 * γ). [INDISCERNABILITY OF IDENTICALS]
  20. From β = (1 * γ), (1 * γ) = γ: deduce β = γ. [INDISCERNABILITY OF IDENTICALS]
  21. QED!
PRODUCT OF INVERTIBLE ELEMENTS IS INVERTIBLE
  • A monoid is like a group, but in which not every element α is invertible in the sense that there is an element X of the monoid for which X * α = 1. A typical example of a monoid is the collection of n × n matrices with (say) real entries, for some fixed n.
  • This exercise asks to prove that if two elements α, β are known to be invertible, then so is their product α * β.
  • The only monoid laws one is given here are the identity law 1 * X = X and the associativity law X * (Y * Z)=(X * Y) * Z, valid for all monoid elements X,Y,Z.
  • As with the other exercises involving actual mathematical objects, one should first sketch out a proof using informal mathematical reasoning, and only then try transferring that proof to the first-order logic deductive system of this text.
  • Technical note: matching for this exercise has not yet been implemented.
  1. FOR ALL X: ((1 * X) = X). [given]
  2. FOR ALL X: (FOR ALL Y: (FOR ALL Z: ((X * (Y * Z)) = ((X * Y) * Z)))). [given]
  3. THERE EXISTS X: ((X * α) = 1). [given]
  4. THERE EXISTS X: ((X * β) = 1). [given]
  5. From THERE EXISTS X: ((X * α) = 1): deduce (x * α) = 1 [setting x s.t. (x * α) = 1]. [EXISTENTIAL INSTANTIATION]
  6. From THERE EXISTS X: ((X * β) = 1): deduce THERE EXISTS X: ((X * β) = 1) [setting x s.t. (x * α) = 1]. [PUSH (for set variables)]
  7. From THERE EXISTS X: ((X * β) = 1) [setting x s.t. (x * α) = 1]: deduce (y * β) = 1 [setting x s.t. (x * α) = 1, setting y s.t. (y * β) = 1]. [EXISTENTIAL INSTANTIATION]
  8. From (x * α) = 1 [setting x s.t. (x * α) = 1]: deduce (x * α) = 1 [setting x s.t. (x * α) = 1, setting y s.t. (y * β) = 1]. [PUSH (for set variables)]
  9. From FOR ALL X: ((1 * X) = X): deduce FOR ALL X: ((1 * X) = X) [setting x s.t. (x * α) = 1, setting y s.t. (y * β) = 1]. [DOUBLE PUSH (for set variables)]
  10. From FOR ALL X: (FOR ALL Y: (FOR ALL Z: ((X * (Y * Z)) = ((X * Y) * Z)))): deduce FOR ALL X: (FOR ALL Y: (FOR ALL Z: ((X * (Y * Z)) = ((X * Y) * Z)))) [setting x s.t. (x * α) = 1, setting y s.t. (y * β) = 1]. [DOUBLE PUSH (for set variables)]
  11. From FOR ALL X: (FOR ALL Y: (FOR ALL Z: ((X * (Y * Z)) = ((X * Y) * Z)))) [setting x s.t. (x * α) = 1, setting y s.t. (y * β) = 1]: deduce FOR ALL Y: (FOR ALL Z: ((x * (Y * Z)) = ((x * Y) * Z))) [setting x s.t. (x * α) = 1, setting y s.t. (y * β) = 1]. [UNIVERSAL SPECIFICATION]
  12. From FOR ALL Y: (FOR ALL Z: ((x * (Y * Z)) = ((x * Y) * Z))) [setting x s.t. (x * α) = 1, setting y s.t. (y * β) = 1]: deduce FOR ALL Z: ((x * (α * Z)) = ((x * α) * Z)) [setting x s.t. (x * α) = 1, setting y s.t. (y * β) = 1]. [UNIVERSAL SPECIFICATION]
  13. From FOR ALL Z: ((x * (α * Z)) = ((x * α) * Z)) [setting x s.t. (x * α) = 1, setting y s.t. (y * β) = 1]: deduce (x * (α * β)) = ((x * α) * β) [setting x s.t. (x * α) = 1, setting y s.t. (y * β) = 1]. [UNIVERSAL SPECIFICATION]
  14. From (x * (α * β)) = ((x * α) * β) [setting x s.t. (x * α) = 1, setting y s.t. (y * β) = 1], (x * α) = 1 [setting x s.t. (x * α) = 1, setting y s.t. (y * β) = 1]: deduce (x * (α * β)) = (1 * β) [setting x s.t. (x * α) = 1, setting y s.t. (y * β) = 1]. [INDISCERNABILITY OF IDENTICALS]
  15. From FOR ALL X: ((1 * X) = X) [setting x s.t. (x * α) = 1, setting y s.t. (y * β) = 1]: deduce (1 * β) = β [setting x s.t. (x * α) = 1, setting y s.t. (y * β) = 1]. [UNIVERSAL SPECIFICATION]
  16. From (x * (α * β)) = (1 * β) [setting x s.t. (x * α) = 1, setting y s.t. (y * β) = 1], (1 * β) = β [setting x s.t. (x * α) = 1, setting y s.t. (y * β) = 1]: deduce (x * (α * β)) = β [setting x s.t. (x * α) = 1, setting y s.t. (y * β) = 1]. [EQUALITY IS TRANSITIVE]
  17. From FOR ALL X: (FOR ALL Y: (FOR ALL Z: ((X * (Y * Z)) = ((X * Y) * Z)))) [setting x s.t. (x * α) = 1, setting y s.t. (y * β) = 1]: deduce FOR ALL Y: (FOR ALL Z: ((y * (Y * Z)) = ((y * Y) * Z))) [setting x s.t. (x * α) = 1, setting y s.t. (y * β) = 1]. [UNIVERSAL SPECIFICATION]
  18. From FOR ALL Y: (FOR ALL Z: ((y * (Y * Z)) = ((y * Y) * Z))) [setting x s.t. (x * α) = 1, setting y s.t. (y * β) = 1]: deduce FOR ALL Z: ((y * (x * Z)) = ((y * x) * Z)) [setting x s.t. (x * α) = 1, setting y s.t. (y * β) = 1]. [UNIVERSAL SPECIFICATION]
  19. From FOR ALL Z: ((y * (x * Z)) = ((y * x) * Z)) [setting x s.t. (x * α) = 1, setting y s.t. (y * β) = 1]: deduce (y * (x * (α * β))) = ((y * x) * (α * β)) [setting x s.t. (x * α) = 1, setting y s.t. (y * β) = 1]. [UNIVERSAL SPECIFICATION]
  20. From (y * (x * (α * β))) = ((y * x) * (α * β)) [setting x s.t. (x * α) = 1, setting y s.t. (y * β) = 1], (x * (α * β)) = β [setting x s.t. (x * α) = 1, setting y s.t. (y * β) = 1]: deduce (y * β) = ((y * x) * (α * β)) [setting x s.t. (x * α) = 1, setting y s.t. (y * β) = 1]. [INDISCERNABILITY OF IDENTICALS]
  21. From (y * β) = 1 [setting x s.t. (x * α) = 1, setting y s.t. (y * β) = 1], (y * β) = ((y * x) * (α * β)) [setting x s.t. (x * α) = 1, setting y s.t. (y * β) = 1]: deduce ((y * x) * (α * β)) = 1 [setting x s.t. (x * α) = 1, setting y s.t. (y * β) = 1]. [INDISCERNABILITY OF IDENTICALS]
  22. From ((y * x) * (α * β)) = 1 [setting x s.t. (x * α) = 1, setting y s.t. (y * β) = 1]: deduce THERE EXISTS X: ((X * (α * β)) = 1) [setting x s.t. (x * α) = 1, setting y s.t. (y * β) = 1]. [EXISTENTIAL INTRODUCTION]
  23. From THERE EXISTS X: ((X * (α * β)) = 1) [setting x s.t. (x * α) = 1, setting y s.t. (y * β) = 1]: deduce THERE EXISTS X: ((X * (α * β)) = 1). [DOUBLE PULL]
  24. QED!
INVERSE IS AN INVOLUTION
  • This is another exercise in group theory. In this exercise, we denote the (left) inverse of a group element X by f(X), thus f(X) * X = 1 for all X.
  • We also are given the associativity law X * (Y * Z)=(X * Y) * Z, the left identity law 1 * X = X, and the right identity law X * 1 = X for all X,Y,Z.
  • The task here is to show that when one applies the inverse operation twice, one ends up where one started: f(f(X)) = X.
  • To get a hint, hover over this sentence.
  • Still stuck? Hover over this sentence.
  • Technical note: matching for this exercise has not yet been implemented.
  1. FOR ALL X: ((1 * X) = X). [given]
  2. FOR ALL X: ((X * 1) = X). [given]
  3. FOR ALL X: (FOR ALL Y: (FOR ALL Z: ((X * (Y * Z)) = ((X * Y) * Z)))). [given]
  4. FOR ALL X: ((f(X) * X) = 1). [given]
  5. From FOR ALL X: ((f(X) * X) = 1): deduce (f(x) * x) = 1 [letting x be arbitrary]. [REVERSE UNIVERSAL INTRODUCTION]
  6. From FOR ALL X: (FOR ALL Y: (FOR ALL Z: ((X * (Y * Z)) = ((X * Y) * Z)))): deduce FOR ALL X: (FOR ALL Y: (FOR ALL Z: ((X * (Y * Z)) = ((X * Y) * Z)))) [letting x be arbitrary]. [PUSH (for free variables)]
  7. From FOR ALL X: (FOR ALL Y: (FOR ALL Z: ((X * (Y * Z)) = ((X * Y) * Z)))) [letting x be arbitrary]: deduce FOR ALL Y: (FOR ALL Z: ((f(f(x)) * (Y * Z)) = ((f(f(x)) * Y) * Z))) [letting x be arbitrary]. [UNIVERSAL SPECIFICATION]
  8. From FOR ALL Y: (FOR ALL Z: ((f(f(x)) * (Y * Z)) = ((f(f(x)) * Y) * Z))) [letting x be arbitrary]: deduce FOR ALL Z: ((f(f(x)) * (f(x) * Z)) = ((f(f(x)) * f(x)) * Z)) [letting x be arbitrary]. [UNIVERSAL SPECIFICATION]
  9. From FOR ALL Z: ((f(f(x)) * (f(x) * Z)) = ((f(f(x)) * f(x)) * Z)) [letting x be arbitrary]: deduce (f(f(x)) * (f(x) * x)) = ((f(f(x)) * f(x)) * x) [letting x be arbitrary]. [UNIVERSAL SPECIFICATION]
  10. From (f(f(x)) * (f(x) * x)) = ((f(f(x)) * f(x)) * x) [letting x be arbitrary], (f(x) * x) = 1 [letting x be arbitrary]: deduce (f(f(x)) * 1) = ((f(f(x)) * f(x)) * x) [letting x be arbitrary]. [INDISCERNABILITY OF IDENTICALS]
  11. From FOR ALL X: ((f(X) * X) = 1): deduce FOR ALL X: ((f(X) * X) = 1) [letting x be arbitrary]. [PUSH (for free variables)]
  12. From FOR ALL X: ((f(X) * X) = 1) [letting x be arbitrary]: deduce (f(f(x)) * f(x)) = 1 [letting x be arbitrary]. [UNIVERSAL SPECIFICATION]
  13. From (f(f(x)) * 1) = ((f(f(x)) * f(x)) * x) [letting x be arbitrary], (f(f(x)) * f(x)) = 1 [letting x be arbitrary]: deduce (f(f(x)) * 1) = (1 * x) [letting x be arbitrary]. [INDISCERNABILITY OF IDENTICALS]
  14. From FOR ALL X: ((1 * X) = X): deduce (1 * x) = x [letting x be arbitrary]. [REVERSE UNIVERSAL INTRODUCTION]
  15. From (f(f(x)) * 1) = (1 * x) [letting x be arbitrary], (1 * x) = x [letting x be arbitrary]: deduce (f(f(x)) * 1) = x [letting x be arbitrary]. [INDISCERNABILITY OF IDENTICALS]
  16. From FOR ALL X: ((X * 1) = X): deduce FOR ALL X: ((X * 1) = X) [letting x be arbitrary]. [PUSH (for free variables)]
  17. From FOR ALL X: ((X * 1) = X) [letting x be arbitrary]: deduce (f(f(x)) * 1) = f(f(x)) [letting x be arbitrary]. [UNIVERSAL SPECIFICATION]
  18. From (f(f(x)) * 1) = x [letting x be arbitrary], (f(f(x)) * 1) = f(f(x)) [letting x be arbitrary]: deduce f(f(x)) = x [letting x be arbitrary]. [INDISCERNABILITY OF IDENTICALS]
  19. From f(f(x)) = x [letting x be arbitrary]: deduce FOR ALL X: (f(f(X)) = X). [ UNIVERSAL INTRODUCTION]
  20. QED!
IRRATIONAL TO IRRATIONAL CAN BE RATIONAL
  • Note: This is one of the hardest exercises in this text; one needs to first think carefully as to how to establish the exercise mathematically, and only then try to translate your mathematical reasoning to a first-order proof.
  • Here, the domain of discourse is intended to be the positive reals, and the predicate R(X) should be interpreted as an assertion that X is a rational number.
  • The task is to show that there exist irrational positive reals X,Y such that the quantity X^Y is rational.
  • As it turns out, this claim can be established using the following relatively elementary facts. Firstly, one needs some laws of exponentiation, namely that (X^Y)^Z = X^(Y*Z), √X * √X = X, and (√X)^2 = X.
  • Secondly, one needs to know that 2 is rational, and √ 2 is irrational.
  • This problem is notable for two reasons. Firstly, and rather surprisingly, the solution relies crucially at one point on the law of the excluded middle!
  • Secondly, you will find at some points in the proof that the law of existential introduction will generate a lot of possible options. One will have to carefully select the right option amongst them!
  • Just a reminder: to apply the law of existential introduction with a specific bound variable, drag the sentence P(α) to the term α, and then CTRL-CLICK on the desired bound variable.
  • To get a hint, hover over this sentence.
  • Still stuck? Hover over this sentence.
  • Thanks to Anders Kaseorg for a short proof.
  • Technical note: matching for this exercise has not yet been implemented.
  1. FOR ALL X: (FOR ALL Y: (FOR ALL Z: (((X ^ Y) ^ Z) = (X ^ (Y * Z))))). [given]
  2. FOR ALL X: ((√(X) * √(X)) = X). [given]
  3. FOR ALL X: ((√(X) ^ 2) = X). [given]
  4. R(2). [given]
  5. NOT R(√(2)). [given]
  6. From FOR ALL X: (FOR ALL Y: (FOR ALL Z: (((X ^ Y) ^ Z) = (X ^ (Y * Z))))): deduce FOR ALL Y: (FOR ALL Z: (((√(2) ^ Y) ^ Z) = (√(2) ^ (Y * Z)))). [UNIVERSAL SPECIFICATION]
  7. From FOR ALL Y: (FOR ALL Z: (((√(2) ^ Y) ^ Z) = (√(2) ^ (Y * Z)))): deduce FOR ALL Z: (((√(2) ^ √(2)) ^ Z) = (√(2) ^ (√(2) * Z))). [UNIVERSAL SPECIFICATION]
  8. From FOR ALL Z: (((√(2) ^ √(2)) ^ Z) = (√(2) ^ (√(2) * Z))): deduce ((√(2) ^ √(2)) ^ √(2)) = (√(2) ^ (√(2) * √(2))). [UNIVERSAL SPECIFICATION]
  9. From ((√(2) ^ √(2)) ^ √(2)) = (√(2) ^ (√(2) * √(2))): deduce (√(2) ^ (√(2) * √(2))) = ((√(2) ^ √(2)) ^ √(2)). [EQUALITY IS SYMMETRIC]
  10. From FOR ALL X: ((√(X) * √(X)) = X): deduce (√(2) * √(2)) = 2. [UNIVERSAL SPECIFICATION]
  11. From FOR ALL X: ((√(X) ^ 2) = X): deduce (√(2) ^ 2) = 2. [UNIVERSAL SPECIFICATION]
  12. From (√(2) ^ (√(2) * √(2))) = ((√(2) ^ √(2)) ^ √(2)), (√(2) * √(2)) = 2: deduce (√(2) ^ 2) = ((√(2) ^ √(2)) ^ √(2)). [INDISCERNABILITY OF IDENTICALS]
  13. From (√(2) ^ 2) = ((√(2) ^ √(2)) ^ √(2)), (√(2) ^ 2) = 2: deduce 2 = ((√(2) ^ √(2)) ^ √(2)). [INDISCERNABILITY OF IDENTICALS]
  14. From R(2), 2 = ((√(2) ^ √(2)) ^ √(2)): deduce R((√(2) ^ √(2)) ^ √(2)). [INDISCERNABILITY OF IDENTICALS]
  15. Deduce R(√(2) ^ √(2)) [assuming R(√(2) ^ √(2))]. [IMPLICATION INTRODUCTION]
  16. From NOT R(√(2)): deduce NOT R(√(2)) [assuming R(√(2) ^ √(2))]. [PUSH]
  17. From NOT R(√(2)) [assuming R(√(2) ^ √(2))], NOT R(√(2)) [assuming R(√(2) ^ √(2))], R(√(2) ^ √(2)) [assuming R(√(2) ^ √(2))]: deduce ((NOT R(√(2))) AND (NOT R(√(2)))) AND R(√(2) ^ √(2)) [assuming R(√(2) ^ √(2))]. [EXERCISE 1.1]
  18. From ((NOT R(√(2))) AND (NOT R(√(2)))) AND R(√(2) ^ √(2)) [assuming R(√(2) ^ √(2))]: deduce THERE EXISTS Y: (((NOT R(√(2))) AND (NOT R(Y))) AND R(√(2) ^ Y)) [assuming R(√(2) ^ √(2))]. [EXISTENTIAL INTRODUCTION]
  19. From THERE EXISTS Y: (((NOT R(√(2))) AND (NOT R(Y))) AND R(√(2) ^ Y)) [assuming R(√(2) ^ √(2))]: deduce THERE EXISTS X: (THERE EXISTS Y: (((NOT R(X)) AND (NOT R(Y))) AND R(X ^ Y))) [assuming R(√(2) ^ √(2))]. [EXISTENTIAL INTRODUCTION]
  20. Deduce NOT R(√(2) ^ √(2)) [assuming NOT R(√(2) ^ √(2))]. [IMPLICATION INTRODUCTION]
  21. From NOT R(√(2)): deduce NOT R(√(2)) [assuming NOT R(√(2) ^ √(2))]. [PUSH]
  22. From R((√(2) ^ √(2)) ^ √(2)): deduce R((√(2) ^ √(2)) ^ √(2)) [assuming NOT R(√(2) ^ √(2))]. [PUSH]
  23. From NOT R(√(2) ^ √(2)) [assuming NOT R(√(2) ^ √(2))], NOT R(√(2)) [assuming NOT R(√(2) ^ √(2))], R((√(2) ^ √(2)) ^ √(2)) [assuming NOT R(√(2) ^ √(2))]: deduce ((NOT R(√(2) ^ √(2))) AND (NOT R(√(2)))) AND R((√(2) ^ √(2)) ^ √(2)) [assuming NOT R(√(2) ^ √(2))]. [EXERCISE 1.1]
  24. From ((NOT R(√(2) ^ √(2))) AND (NOT R(√(2)))) AND R((√(2) ^ √(2)) ^ √(2)) [assuming NOT R(√(2) ^ √(2))]: deduce THERE EXISTS Y: (((NOT R(√(2) ^ √(2))) AND (NOT R(Y))) AND R((√(2) ^ √(2)) ^ Y)) [assuming NOT R(√(2) ^ √(2))]. [EXISTENTIAL INTRODUCTION]
  25. From THERE EXISTS Y: (((NOT R(√(2) ^ √(2))) AND (NOT R(Y))) AND R((√(2) ^ √(2)) ^ Y)) [assuming NOT R(√(2) ^ √(2))]: deduce THERE EXISTS X: (THERE EXISTS Y: (((NOT R(X)) AND (NOT R(Y))) AND R(X ^ Y))) [assuming NOT R(√(2) ^ √(2))]. [EXISTENTIAL INTRODUCTION]
  26. From THERE EXISTS X: (THERE EXISTS Y: (((NOT R(X)) AND (NOT R(Y))) AND R(X ^ Y))) [assuming R(√(2) ^ √(2))], THERE EXISTS X: (THERE EXISTS Y: (((NOT R(X)) AND (NOT R(Y))) AND R(X ^ Y))) [assuming NOT R(√(2) ^ √(2))]: deduce THERE EXISTS X: (THERE EXISTS Y: (((NOT R(X)) AND (NOT R(Y))) AND R(X ^ Y))). [EXCLUDED MIDDLE (case analysis form)]
  27. QED!
  • This is a variant of Exercise 24.4. One is given the left identity, associativity, and left inverse properties of a group, and one has to derive the right identity property.
  • Thanks to Martin Epstein for suggesting this exercise.
  • Stuck? Hover over this sentence.
  • Thanks to Anders Kaseorg for a short proof, Martin Epstein for a shorter proof, and Anders Kaseorg for an even shorter proof.
  • Technical note: matching for this exercise has not yet been implemented.
  1. FOR ALL X: ((1 * X) = X). [given]
  2. FOR ALL X: (FOR ALL Y: (FOR ALL Z: ((X * (Y * Z)) = ((X * Y) * Z)))). [given]
  3. FOR ALL X: (THERE EXISTS Y: ((Y * X) = 1)). [given]
  4. From FOR ALL X: (THERE EXISTS Y: ((Y * X) = 1)): deduce THERE EXISTS Y: ((Y * α) = 1). [UNIVERSAL SPECIFICATION]
  5. From THERE EXISTS Y: ((Y * α) = 1): deduce (x * α) = 1 [setting x s.t. (x * α) = 1]. [EXISTENTIAL INSTANTIATION]
  6. From FOR ALL X: (THERE EXISTS Y: ((Y * X) = 1)): deduce FOR ALL X: (THERE EXISTS Y: ((Y * X) = 1)) [setting x s.t. (x * α) = 1]. [PUSH (for set variables)]
  7. From FOR ALL X: (THERE EXISTS Y: ((Y * X) = 1)) [setting x s.t. (x * α) = 1]: deduce THERE EXISTS Y: ((Y * x) = 1) [setting x s.t. (x * α) = 1]. [UNIVERSAL SPECIFICATION]
  8. From THERE EXISTS Y: ((Y * x) = 1) [setting x s.t. (x * α) = 1]: deduce (y * x) = 1 [setting x s.t. (x * α) = 1, setting y s.t. (y * x) = 1]. [EXISTENTIAL INSTANTIATION]
  9. From FOR ALL X: (FOR ALL Y: (FOR ALL Z: ((X * (Y * Z)) = ((X * Y) * Z)))): deduce FOR ALL X: (FOR ALL Y: (FOR ALL Z: ((X * (Y * Z)) = ((X * Y) * Z)))) [setting x s.t. (x * α) = 1, setting y s.t. (y * x) = 1]. [DOUBLE PUSH (for set variables)]
  10. From FOR ALL X: (FOR ALL Y: (FOR ALL Z: ((X * (Y * Z)) = ((X * Y) * Z)))) [setting x s.t. (x * α) = 1, setting y s.t. (y * x) = 1]: deduce FOR ALL Y: (FOR ALL Z: ((y * (Y * Z)) = ((y * Y) * Z))) [setting x s.t. (x * α) = 1, setting y s.t. (y * x) = 1]. [UNIVERSAL SPECIFICATION]
  11. From FOR ALL Y: (FOR ALL Z: ((y * (Y * Z)) = ((y * Y) * Z))) [setting x s.t. (x * α) = 1, setting y s.t. (y * x) = 1]: deduce FOR ALL Z: ((y * (1 * Z)) = ((y * 1) * Z)) [setting x s.t. (x * α) = 1, setting y s.t. (y * x) = 1]. [UNIVERSAL SPECIFICATION]
  12. From FOR ALL Z: ((y * (1 * Z)) = ((y * 1) * Z)) [setting x s.t. (x * α) = 1, setting y s.t. (y * x) = 1]: deduce (y * (1 * 1)) = ((y * 1) * 1) [setting x s.t. (x * α) = 1, setting y s.t. (y * x) = 1]. [UNIVERSAL SPECIFICATION]
  13. From FOR ALL X: ((1 * X) = X): deduce FOR ALL X: ((1 * X) = X) [setting x s.t. (x * α) = 1, setting y s.t. (y * x) = 1]. [DOUBLE PUSH (for set variables)]
  14. From FOR ALL X: ((1 * X) = X) [setting x s.t. (x * α) = 1, setting y s.t. (y * x) = 1]: deduce (1 * 1) = 1 [setting x s.t. (x * α) = 1, setting y s.t. (y * x) = 1]. [UNIVERSAL SPECIFICATION]
  15. From (y * (1 * 1)) = ((y * 1) * 1) [setting x s.t. (x * α) = 1, setting y s.t. (y * x) = 1], (1 * 1) = 1 [setting x s.t. (x * α) = 1, setting y s.t. (y * x) = 1]: deduce (y * 1) = ((y * 1) * 1) [setting x s.t. (x * α) = 1, setting y s.t. (y * x) = 1]. [INDISCERNABILITY OF IDENTICALS]
  16. From (x * α) = 1 [setting x s.t. (x * α) = 1]: deduce (x * α) = 1 [setting x s.t. (x * α) = 1, setting y s.t. (y * x) = 1]. [PUSH (for set variables)]
  17. From FOR ALL Y: (FOR ALL Z: ((y * (Y * Z)) = ((y * Y) * Z))) [setting x s.t. (x * α) = 1, setting y s.t. (y * x) = 1]: deduce FOR ALL Z: ((y * (x * Z)) = ((y * x) * Z)) [setting x s.t. (x * α) = 1, setting y s.t. (y * x) = 1]. [UNIVERSAL SPECIFICATION]
  18. From FOR ALL Z: ((y * (x * Z)) = ((y * x) * Z)) [setting x s.t. (x * α) = 1, setting y s.t. (y * x) = 1]: deduce (y * (x * α)) = ((y * x) * α) [setting x s.t. (x * α) = 1, setting y s.t. (y * x) = 1]. [UNIVERSAL SPECIFICATION]
  19. From (y * (x * α)) = ((y * x) * α) [setting x s.t. (x * α) = 1, setting y s.t. (y * x) = 1], (x * α) = 1 [setting x s.t. (x * α) = 1, setting y s.t. (y * x) = 1]: deduce (y * 1) = ((y * x) * α) [setting x s.t. (x * α) = 1, setting y s.t. (y * x) = 1]. [INDISCERNABILITY OF IDENTICALS]
  20. From (y * 1) = ((y * x) * α) [setting x s.t. (x * α) = 1, setting y s.t. (y * x) = 1], (y * x) = 1 [setting x s.t. (x * α) = 1, setting y s.t. (y * x) = 1]: deduce (y * 1) = (1 * α) [setting x s.t. (x * α) = 1, setting y s.t. (y * x) = 1]. [INDISCERNABILITY OF IDENTICALS]
  21. From FOR ALL X: ((1 * X) = X) [setting x s.t. (x * α) = 1, setting y s.t. (y * x) = 1]: deduce (1 * α) = α [setting x s.t. (x * α) = 1, setting y s.t. (y * x) = 1]. [UNIVERSAL SPECIFICATION]
  22. From (y * 1) = (1 * α) [setting x s.t. (x * α) = 1, setting y s.t. (y * x) = 1], (1 * α) = α [setting x s.t. (x * α) = 1, setting y s.t. (y * x) = 1]: deduce (y * 1) = α [setting x s.t. (x * α) = 1, setting y s.t. (y * x) = 1]. [EQUALITY IS TRANSITIVE]
  23. From (y * 1) = ((y * 1) * 1) [setting x s.t. (x * α) = 1, setting y s.t. (y * x) = 1], (y * 1) = α [setting x s.t. (x * α) = 1, setting y s.t. (y * x) = 1]: deduce α = (α * 1) [setting x s.t. (x * α) = 1, setting y s.t. (y * x) = 1]. [INDISCERNABILITY OF IDENTICALS]
  24. From α = (α * 1) [setting x s.t. (x * α) = 1, setting y s.t. (y * x) = 1]: deduce (α * 1) = α [setting x s.t. (x * α) = 1, setting y s.t. (y * x) = 1]. [EQUALITY IS SYMMETRIC]
  25. From (α * 1) = α [setting x s.t. (x * α) = 1, setting y s.t. (y * x) = 1]: deduce (α * 1) = α. [DOUBLE PULL]
  26. QED!